Totality & Termination

























Totality Checking


Liquid Haskell compains on partial functions.


module TotalityAndTermination where {-@ myHead :: [a] -> a @-} myHead :: [a] -> a myHead (x:_) = x

Similar to ghc -W's

    Pattern match(es) are non-exhaustive
    In an equation for ‘myHead’: Patterns not matched: []
   |
46 | myHead (x:_) = x
   | ^^^^^^^^^^^^^^^^













Liquid Haskell vs. ghc on totality

  • [❤ ghc] ghc tells you the missing patterns

  • [❤ LH] Liquid Haskell allows for Haskell partial functions

{-@ myHead :: xs:{[a] | 0 < len xs } -> a @-}
  • [❤ LH] Liquid Haskell knowns logic, e.g., ghc complains in the below
{-@ swap :: Ord a => [a] -> [a] @-} swap :: Ord a => [a] -> [a] swap [] = [] swap [x] = [x] swap (x:y:zs) | x <= y = x:y:zs | y < x = y:x:zs 
  Pattern match(es) are non-exhaustive
  In an equation for ‘swap’: Patterns not matched: (_:_:_)

Q: What if the input list is ordered, encoded as OList a?










Liquid Haskell also checks termination


Q: Does fib terminate?

{-@ fib :: i:Int -> Int @-} fib :: Int -> Int fib i | i == 0 = 0 | i == 1 = 1 | otherwise = fib (i-1) + fib (i-2)













Liquid Haskell's termination heuristic


  • Check that the first inductive argument is decreasing at each recursive call.

  • If the check fails, then

    • a terminating error is created and
    • the user can "explain" the termination argument.













Temination explanation

{-@ merge :: Ord a => [a] -> [a] -> [a] @-} merge :: Ord a => [a] -> [a] -> [a] merge xs [] = xs merge [] ys = ys merge (x:xs) (y:ys) | x <= y = x:merge xs (y:ys) | y < x = y:merge xs ys


Q: Can you spot the merge error?

Q: Does it still terminate?

Q: Let's prove the result is ordered (OList a) too!













Recap

  • Liquid Haskell checks, by default, termination & totality.

  • You can deactivate it via --no-termination and --no-totality, resp..

  • Observation: Functions that are total & terminating are really math functions! Let's use them to encode proofs!













Appendix

{-@ type OList a = [a]<{\x v -> x <= v}> @-}