非穷尽模式匹配为什么会导致不可避免的模式匹配失败？

Question

非穷尽模式匹配为什么会导致不可避免的模式匹配失败？

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没有失败第一个模式，而是匹配了第二个模式。我期望会出现某种错误——也许是“非详尽保护”。所以这里到底发生了什么，有没有办法在这种情况下启用编译器警告？

- Matt Fenwick

3个回答

6

编译器应该会警告您，如果省略了第二个子句，也就是说，如果您的最后一个匹配具有一组卫语句，其中最后一个不是平凡真值。

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

回答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

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

- Ingo

你能详细解释一下为什么这不可能吗？我熟悉停机问题，但不明白为什么显然不可能。 - Matt Fenwick

我喜欢使用Fermat's Last Theorem作为例子。对于不熟悉的人来说，这是数学中最著名的问题之一，在1995年才被证明（尽管费马声称有一个证明，但太大了无法放入页边距内）。 - hammar

在类型类的存在下，情况会更糟。在您的第一个示例中，编译器必须证明a <= b或a > b其中之一，甚至没有<=或>的实现可用！（事实上，证明这一点显然是不可能的，因为在面对编写不良的实例时，它甚至不一定成立。） - Daniel Wagner

@Daniel - 非常正确。虽然有人可能会争论，如果能够证明或证伪像 forall x.p x || q x 这样的定理，那么通过规律实例必须遵循的方式来丰富类定义也是可能的，并且是一个很好的特性，例如 _forall a b. a < b && not (b <= a) || a >= b && not (b > a)_。 - Ingo

在编译器中做那是不可能的。我确定它并非完全“不可能”，只是不切实际。 - Thomas Eding

1

守卫并不是不可辩驳的。但是很常见（也是好的）做法是添加一个最后的守卫来捕获其他情况，这样你的函数就变成了：

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

- Mariy

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- hammar · Accepted Answer

第一个模式确实是一个"无法反驳的模式"，但这并不意味着它总是会选择函数对应的右侧。它仍然受到保护条件的限制，就像在您的示例中一样可能失败。

为了确保覆盖所有情况，通常使用otherwise来添加最终保护条件以保证始终成功。

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

注意，otherwise 没有什么神奇之处。它在Prelude中定义为 otherwise = True。然而，在最后的情况下使用 otherwise 是惯用的。

编译器警告非全面性保护是不可能的，因为它涉及到解决停机问题，但存在像Catch这样的工具，试图比编译器更好地确定在常见情况下是否覆盖了所有情况。