haskell - 有没有什么工具可以进行防守分析？

Question

我是一个 Haskell 新手，在阅读 Haskell Road 中的含义时，我遇到了以下难题。

verdict :: Bool -> Bool -> (Bool, String)
verdict p q | not result  = (False, "LIAR")
            | result && p = (True,  "telling the truth")
            | result      = (True,  "innocent unless proven guilty")
            | otherwise   = (False, "we shouldn't get here")
  where result = (not p) || q
-- map (\x -> verdict (fst x == 1) (snd x == 1)) [(1,1),(1,0),(0,1),(0,0)]

是否有工具可以警告我其他或其他类似的逻辑错误？

Answer 1

我想我会以不同的方式编写这个函数:

-- not result
verdict True  False = (False, "LIAR")
-- result && p
verdict True  True  = (True , "telling the truth")
-- result
verdict False _     = (True , "innocent unless proven guilty")
verdict _     True  = (True , "innocent unless proven guilty")
-- otherwise
verdict _     _     = (False, "we shouldn't get here")

那么不仅对于人类来说哪些子句可以被省略(最后两个)是显而易见的，而且对于机器来说也是如此； ghc 在默认警告级别表示:

test.hs:2:5: Warning:
    Pattern match(es) are overlapped
    In an equation for ‘verdict’:
        verdict _ True = ...
        verdict _ _ = ...

检查守卫重叠通常是不可判定的；而且我不知道有什么工具可以尝试给出近似答案。