彻底的卫兵造成无可辩驳的模式匹配失败？

2018-06-15 05:52:15

我在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不会失败的第一个模式，并匹配第二个。我预计会出现某种错误 - 也许是“非穷举的守卫”。那么这里究竟发生了什么，有没有办法在发生这种意外情况时启用编译器警告？

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

为了确保涵盖所有的情况，通常使用otherwise来获得总是成功的最终后卫。

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

请注意，没有什么神奇的约otherwise 。它在Prelude中定义为otherwise = True 。然而，这是惯用的使用otherwise对于最后一种情况。

在一般情况下，编译器会警告有关非限制性警卫是不可能的，因为它会涉及解决暂停问题，但是存在像Catch这样的工具，它们试图比编译器在确定是否覆盖所有情况方面做得更好，或者不是在一般情况下。

如果你忽略了第二个条款，编译器应该警告你，即如果你的最后一场比赛有一组守卫，而最后一场比赛不是平凡的话。

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

回答Matt的评论：

看看这个例子：

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

编译器必须证明，如果px不是最低点，那么px对所有可能的x都为True 。换句话说，无论x是什么或评价为True ，它都必须证明px是底部的（不停止）。

卫兵不是无可辩驳的。但是，添加最后一个守卫来捕获其他案例是非常常见的（也是很好的）做法，所以你的功能变为：

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

链接地址: http://www.djcxy.com/p/43275.html