{-# LANGUAGE TupleSections #-}
{-@ LIQUID "--no-warnings" @-}
{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--totality" @-}
{-@ LIQUID "--diff" @-}
module Termination where
import Prelude hiding (map, repeat)
fib :: Int -> Int
map :: (a -> b) -> [a] -> [b]
isOdd, isEven :: Int -> Bool
ack :: Int -> Int -> Int
range :: Int -> Int -> [Int]

LiquidHaskell checks *by default* that all your functions terminate!

Why?

- It is the
*expected*case! - For soundness: Refinement Types for Haskell

`fib`

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

**Q:** Why is there an error?

Liquid Haskell checks a *well founded* metric decreases at each recursive call.

*Well founded* metrics:

- the first integer argument.

The first integer is not always decreasing!

{-@ range :: lo:Int -> hi:Int -> [Int] / [0] @-}
range lo hi
| lo < hi = lo : range (lo+1) hi
| otherwise = []

**Q:** Replace `0`

with the decreasing metric!

Liquid Haskell checks a *well founded* metric decreases at each recursive call.

*Well founded* metrics:

- user specified metrics, or
- the first integer argument.

Why does Ackermann Function terminate?

{-@ ack :: m:Int -> n:Int -> Int / [0, 0] @-}
ack m n
| m == 0 = n + 1
| n == 0 = ack (m-1) 1
| otherwise = ack (m-1) (ack m (n-1))

**Q:** Replace `0`

with the decreasing *metrics*!

Map ADTs to integers using measures!

{-@ map :: (a -> b) -> xs:[a] -> [b] / [len xs] @-}
map _ [] = []
map f (x:xs) = f x : map f xs

But Liquid Haskell knows that!

It will use `len`

as the default metric to check `x:[a]`

decreasing.

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

Does `merge`

terminate?

Liquid Haskell cannot know that!

Same idea generalizes to mutual recursion.

{-@ isEven :: n:Nat -> Bool / [n, 0] @-}
{-@ isOdd :: m:Nat -> Bool / [m, 0] @-}
isEven 0 = True
isEven n = isOdd (n-1)
isOdd m = not $ isEven m

Can you find the correct metric?

Liquid Haskell does not even attempt to guess it...

`lazy`

annotation deactivates termination checking.

{-@ lazy repeat @-}
repeat x = x:repeat x

For non `Lazy`

specified functions,

Liquid Haskell checks a *well founded* metric decreases at each recursive call.

*Well founded* metrics:

- user specified
*lexocographic*metrics, - the first integer or "sized" argument.

**Refinements:**Types + Predicates**Subtyping:**SMT Implication**Measures:**Specify Properties of Data**Termination:**Use Logic to Prove Termination

What properties can be expressed in the logic?

Linear Arithmetic, Booleans, Uninterpreted Functions, ... (SMT logic)

Terminating Haskell functions.

**Next:** Refinement Reflection