exhaustive guards cause irrefutable pattern match to fail?
I have this function in Haskell:
test :: (Eq a) => a -> a -> Maybe a
test a b
| a == b = Just a
test _ _ = Nothing
This is what I got when I tried the function with different inputs:
ghci>test 3 4
Nothing
ghci>test 3 3
Just 3
According to Real World Haskell, the first pattern is irrefutable. But it seems like test 3 4 doesn't fails the first pattern, and matches the second. I expected some kind of error -- maybe 'non-exhaustive guards'. So what is really going on here, and is there a way to enable compiler warnings in case this accidentally happens?
The first pattern is indeed an "irrefutable pattern", however this does not mean that it will always choose the corresponding right hand side of your function. It is still subject to the guard which may fail as it does in your example.
To ensure all cases are covered, it is common to use otherwise to have a final guard which will always succeed.
test :: (Eq a) => a -> a -> Maybe a
test a b
| a == b = Just a
| otherwise = Nothing
Note that there is nothing magic about otherwise . It is defined in the Prelude as otherwise = True . However, it is idiomatic to use otherwise for the final case.
Having a compiler warn about non-exaustive guards would be impossible in the general case, as it would involve solving the halting problem, however there exist tools like Catch which attempt to do a better job than the compiler at determining whether all cases are covered or not in the common case.
The compiler should be warning you if you leave out the second clause, ie if your last match has a set of guards where the last one is not trivially true.
Generally, testing guards for completeness is obviously not possible, as it would be as hard as solving the halting problem.
Answer to Matt's comment:
Look at the example:
foo a b
| a <= b = True
| a > b = False
A human can see that one of both guards must be true. But the compiler does not know that either a <= b or a > b .
Now look for another example:
fermat a b c n
| a^n + b^n /= c^n = ....
| n < 0 = undefined
| n < 3 = ....
To prove that the set of guards is complete, the compiler had to prove Fermat's Last Theorem. It's impossible to do that in a compiler. Remember that the number and complexity of the guards is not limited. The compiler would have to be a general solver for mathematical problems, problems that are stated in Haskell itself.
More formally, in the easiest case:
f x | p x = y
the compiler must prove that if px is not bottom, then px is True for all possible x. In other words, it must prove that either px is bottom (does not halt) no matter what x is or evaluates to True .
Guards aren't irrefutable. But is very common (and good) practise to add one last guard that catch the other cases, so your function becomes:
test :: (Eq a) => a -> a -> Maybe a
test a b
| a == b = Just a
| True = Nothing
上一篇: 功能上的详尽模式
下一篇: 彻底的卫兵造成无可辩驳的模式匹配失败？