为什么非详尽的警卫导致无可辩驳的模式匹配失败？

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

根据Real World 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这样的工具,它们试图在确定所有案例是否被覆盖时是否比编译器做得更好或者不是常见的情况.

@Matt:模式确实匹配,然后由它绑定的任何变量都可用于后卫,然后可能会失败.发生这种情况时,将按顺序尝试剩余的警卫.如果它们全部失败,则尝试下一个模式.如果没有剩余的模式可供尝试,则会出现非详尽的模式匹配错误. (4认同)
在GHC中``否则'*是*特殊的.如果您尝试自己定义它,最终会得到非详尽的匹配编译时警告(当然,只要您启用这些警告). (4认同)

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不是底部,则p x是True对所有可能的X.换句话说,它必须证明无论p x是什么x或评估,它们都是底部(不停止)True.