15

考虑以下代码：

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1

尽管fun是一个详尽的匹配项，但在使用 -Wall 编译时，GHC 会抱怨缺少案例。但是，如果我添加另一个构造函数：

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl Baz) = 2

然后 GHC 正确地检测到乐趣是全部的。

我在我的工作中使用了与此类似的代码，并且希望 GHC 在我错过案例时发出警告，如果我没有，则不发出警告。为什么 GHC 抱怨第一个程序，我怎样才能在不添加虚假构造函数或案例的情况下编译第一个示例而不发出警告？

4

3 回答 3

13

实际报告的问题是：

Warning: Pattern match(es) are non-exhaustive
         In an equation for `fun': Patterns not matched: Inl _

这是真的。您为构造函数提供了一个案例Inr，但没有为Inl构造函数提供案例。

您希望的是，由于无法提供Sig B使用Inl构造函数的 type 值（它需要 type 的参数Foo B，但唯一的构造函数Foo是 type Foo A），因此 ghc 会注意到您不需要处理Inl构造函数。

麻烦的是，由于底部，每种类型都有人居住。有使用构造函数的类型值Sig B；Inl甚至还有非底部值。它们必须包含底部，但它们本身不是底部。因此，程序可能会评估对fun不匹配的调用；这就是 ghc 的警告。

因此，要解决此问题，您需要更改fun为以下内容：

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl foo) = error "whoops"

但是现在当然如果你以后添加Baz :: Foo B这个功能是一个等待发生的定时炸弹。ghc 对此发出警告是件好事，但实现这一点的唯一方法是foo针对当前详尽的一组模式进行模式匹配。不幸的是，没有有效的模式可以放在那里！foo已知是 type Foo B，它只存在于底部，不能为底部编写模式。

但是你可以将它传递给一个接受多态类型参数的函数Foo a。然后，该函数可以匹配所有当前存在的Foo构造函数，因此如果您稍后添加一个构造函数，您将收到警告。像这样的东西：

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl foo) = errorFoo foo
    where 
        errorFoo :: Foo a -> b
        errorFoo Foo = error "whoops"

现在您已经正确处理了:+:infun的所有构造函数，“不可能”的情况只会出错，如果它确实发生过，并且如果您添加过，Baz :: Foo B您会收到关于 in 的非详尽模式的警告errorFoo，这至少会引导您查看atfun因为它是在附件中定义的where。

不利的一面是，当您向Foo（比如更多类型Foo A）添加不相关的构造函数时，您必须向 中添加更多案例errorFoo，如果您有很多应用这种模式的函数，那可能会很不有趣（尽管简单且机械）。

于 2013-04-26T01:10:28.113 回答
7

很抱歉告诉你这个，但你的第一个例子并不像你想象的那么详尽：

∀x. x ⊢ fun (Inl (undefined :: Foo B))
*** Exception: Test.hs:48:1-17: Non-exhaustive patterns in function fun

烦人，是的，但它们是休息时间。⊥ 是我们不能拥有美好事物的原因。:[

于 2013-04-25T22:53:04.687 回答
1

如前所述。您不处理的情况是Inl _|_，它本身不是_|_，因此必须处理。

幸运的是，有一种非常好的方法来处理这个问题：


data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl x) = case x of {}

现在，如果您确实添加了Baz :: Foo B构造函数，您将适当地得到：

    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: Baz
   |
21 | fun (Inl x) = case x of {}
   |               ^^^^

因此，您可以适当地将代码更改为类似于第二个示例的代码，以正确处理您创建的新案例。

于 2019-02-11T20:26:26.467 回答