为什么非穷举防护会导致无可辩驳的模式匹配失败？

Question

我在 Haskell 中有这个函数：

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b = Just a
test _ _ = Nothing

这是当我尝试使用不同输入的函数时得到的结果：

ghci>test 3 4
Nothing
ghci>test 3 3
Just 3

根据现实世界的 Haskell，第一个模式是无可辩驳的。但似乎 test 3 4 没有使第一个模式失败，并且匹配第二个模式。我预计会出现某种错误——也许是“非详尽的守卫”。那么这里到底发生了什么，有没有办法启用编译器警告，以防意外发生？

Answer 1

第一个模式确实是一个“无可辩驳的模式”，但这并不意味着它总是选择函数相应的右侧。它仍然受到警卫的影响，这可能会像您的示例中那样失败。

为了确保覆盖所有情况，通常使用 otherwise 来拥有一个始终会成功的最终防护。

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b    = Just a
  | otherwise = Nothing

请注意，otherwise 并没有什么神奇之处。它在 Prelude 中被定义为 otherwise = True。但是，对于最终情况，通常使用otherwise。

在一般情况下，让编译器警告非详尽的保护是不可能的，因为这将涉及解决停止问题，但是存在诸如 Catch 试图比编译器做得更好，以确定在常见情况下是否涵盖所有情况。

Answer 2

如果您遗漏了第二个子句，即如果您的最后一个匹配有一组守卫，其中最后一个不完全正确，编译器应该警告您。

一般来说，测试守卫的完整性显然是不可能的，因为这与解决停止问题一样困难。

回答马特的评论：

看这个例子：

foo a b 
   | a <= b = True
   | a >  b = False

一个人可以看到两个守卫之一一定是真的。但编译器不知道 a <= b 或 a > 。 b.。

现在看另一个例子：

fermat a b c n 
    | a^n + b^n /= c^n = ....
    | n < 0 = undefined
    | n < 3 = ....

为了证明守卫集合是完整的，编译器必须证明费马大定理。在编译器中不可能做到这一点。请记住，防护装置的数量和复杂性是不受限制的。编译器必须是数学问题的通用求解器，这些问题在 Haskell 本身中陈述。

更正式地说，在最简单的情况下：

 f x | p x = y

编译器必须证明如果 p x 不是底部，则对于所有可能的 x，p x 都是 True。换句话说，它必须证明无论 x 是什么或计算结果为 True，p x 都是底部（不会停止）。

Answer 3

守卫并不是无可辩驳的。但是添加最后一个防护来捕获其他情况是非常常见（也是好的）做法，因此您的函数变为：

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b = Just a
  | True = Nothing