11

我在 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

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

4

3 回答 3

12

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

为了确保涵盖所有情况，通常使用otherwise最终的守卫，它总是会成功。

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

请注意，没有什么神奇的otherwise。它在 Prelude 中被定义为otherwise = True. otherwise但是，用于最后一种情况是惯用的。

在一般情况下，让编译器警告非详尽的保护是不可能的，因为这将涉及解决停止问题，但是存在像Catch这样的工具，它们试图在确定是否所有情况都被覆盖或不是在普通情况下。

于 2011-08-18T14:52:36.180 回答
6

如果你遗漏了第二个子句，编译器应该会警告你，即如果你的最后一个匹配有一组保护，而最后一个不是真的。

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

回答马特的评论：

看例子：

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不是底部，那么p x对于True所有可能的x。换句话说，它必须证明无论是什么或评估为什么，要么p x是底部（不停止）。 xTrue

于 2011-08-18T15:10:55.433 回答
1

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

test :: (Eq a) => a -> a -> Maybe a
test a b
  | a == b = Just a
  | True = Nothing
于 2011-08-18T14:52:32.047 回答