为什么这个功能不详尽？

Question

编译器警告函数"insert"在以下代码中并非详尽无遗:

data Set a = Empty | Set a (Set a) (Set a) deriving (Eq, Show)

insert :: (Ord a) => a -> Set a -> Set a
insert x Empty = Set x Empty Empty
insert x (Set v l r)
  | x <= v = Set v (insert x l) r
  | v < x  = Set v l (insert x r)
--  | otherwise = Set x Empty Empty

main :: IO ()
main = do
  let x = insert (5::Int) Empty
  print x

GHC报告了这一点

test.hs:4:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘insert’: Patterns not matched: _ (Set _ _ _)

如果我在函数中取消注释最后一行(现在已注释掉),GHC不会报告任何警告.所以我猜GHC认为警卫并非详尽无遗.但为什么？如果x和v是Ord的实例,那么我猜(x <= v)和(v <x)是比较的所有可能结果？

Answer 1

如果我定义这个实例怎么办:

newtype Fuzzy = Fuzzy Double
instance Eq Fuzzy where
  Fuzzy a == Fuzzy b = abs (a-b) < 0.1
instance Ord Fuzzy where
  Fuzzy a < Fuzzy b = a < b-0.1
  Fuzzy a <= Fuzzy b = a <= b

那么对于例如v = Fuzzy 0,x = Fuzzy 0.1你有(x <= v) = (0.1 <= 0)哪些是假的,但(v < x) = (0 < 0)它也是假的.因此,你的两个守卫都会失败.

这不是假设,事实上Double它本身已经具有退化价值的这种行为:

Prelude> sqrt (-1) < 0
False
Prelude> 0 <= sqrt (-1)
False

现在,这些是否真的很好,甚至构造良好的Ord实例都是值得商榷的,但无论如何编译器都无法保证这样的事情不会发生.因此它也不能做出not (x <= v)暗示的假设v < x,那么如果两者都没有实现会发生什么呢？

如果你假设Ord你收到的所有实例都是温顺的话,通常要做的就是让第二个句子已经全部:

insert x (Set v l r)
  | x <= v     = Set v (insert x l) r
  | otherwise  = Set v l (insert x r)

但是,根据您的理念,您的原始代码可能实际上更好.如果有人拿到你的NaN值,你只需要推迟这种怪异.这使得理解正在发生的事情变得更加困难.

如果在实验代码中倾向于故意不完全使用"不可能的情况"模式:这样我至少总会得到一个明确的运行时错误,告诉我代码中的哪一点出错了.一旦代码基本上是工作,你希望把它生产就绪,你可以再折腾-Wall和了解所有的斑点,你最好加就像我提到的一种病理性行为的一些明确的处理.