7

给定以下程序：

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B
type family IsA (foo :: Foo) :: Bool

type instance IsA A = True
type instance IsA B = False

data Bar (foo :: Foo) where
    BarA :: (IsA foo ~ True) => Int -> Bar foo
    BarB :: (IsA foo ~ False) => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x

用于上面定义-fwarn-incomplete-patterns的总功能时，我从 GHC 7.4.2 收到此警告：f

Warning: Pattern match(es) are non-exhaustive
         In a case alternative: Patterns not matched: BarB _

当然，即使尝试添加匹配项也是没有意义的BarB：

Couldn't match type `'False' with `'True'
Inaccessible code in
  a pattern with constructor
    BarB :: forall (foo :: Foo). IsA foo ~ 'False => String -> Bar foo,
  in a case alternative
In the pattern: BarB _
In a case alternative: BarB _ -> undefined
In the expression:
  case bar of {
    BarA x -> x
    BarB _ -> undefined }

有没有办法说服 GHCf是完全的？另外，这是 GHC 的一个错误，还是只是一个已知的限制？或者实际上有一个很好的理由为什么没有办法看到模式匹配f是完整的？

4

2 回答 2

9

这很烦人，是的。GHC 假设类型族（和类）在其算法中是开放的。但是，您正在编写由封闭类型参数化的类型族。这种紧张关系解释了你和 GHC 之间的误解。我认为已经有一些关于如何处理封闭类型课程和家庭的想法，但这是一个棘手的领域。

同时，您可以避免类型族的开放性以说服整体检查器。

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B

data Bar (foo :: Foo) where
    BarA :: Int    -> Bar A -- or BarA :: foo ~ A => Int    -> Bar foo
    BarB :: String -> Bar B -- or BarB :: foo ~ B => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x
-- or f (BarA x) = x
于 2012-09-15T18:04:40.347 回答
1

您始终可以使用_模式匹配任何内容作为案例的最后一个条件。

所以_ -> undefined代替BarB _ -> undefined.

这将使案例在其论点中变得完整。

还有一个由 Neil Mitchell 编写的库，它检查非详尽模式以防止由于模式不匹配而导致运行时失败。

于 2012-09-15T16:14:01.490 回答