Measures

7: module Measures where
8: import Prelude hiding ((!!), length)
9: import Language.Haskell.Liquid.Prelude
10: 
11: {-@ LIQUID "--no-termination" @-}

Measuring A List's length in logic

On List data type

20: infixr `C`
21: data L a = N | C a (L a)

We define a measure for the length of a List

27: {-@ measure llen :: (L a) -> Int
28:     llen(N)      = 0
29:     llen(C x xs) = 1 + (llen xs)
30:   @-}

36: data L a where 
37:   N :: {v : L a | (llen v) = 0}
38:   C :: x:a -> xs:(L a) -> {v:(L a) |(llen v) = 1 + (llen xs)}

Measuring A List's length in logic

And we can type (!!) as

50: {-@ (!!)     :: ls:(L a) -> i:{v:Nat | v < (llen ls)} -> a @-}
51: (!!)         :: L a -> Int -> a
52: (C x _) forall a.
x1:(Measures.L a)
-> {v : GHC.Types.Int | (v >= 0) && (v < (llen x1))} -> a!! 0 = {VV : a | (VV == x)}x
53: (C _ xs)!! n = (Measures.L {VV : a | (x <= VV)})xsforall a.
x1:(Measures.L a)
-> {v : GHC.Types.Int | (v >= 0) && (v < (llen x1))} -> a!!({x2 : GHC.Types.Int | (x2 >= 0)}nx1:GHC.Types.Int
-> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 - x2))}-{x2 : GHC.Types.Int | (x2 == (1  :  int))}1)
54: _       !! _ = {x1 : [GHC.Types.Char] | false} -> aliquidError {x2 : [GHC.Types.Char] | ((len x2) >= 0)}"index too large"

Demo: Lets see what happens if we change the precondition

Another measure for List

We define a new measure to check nullity of a List

69: {-@ measure isNull :: (L a) -> Prop
70:     isNull(N)      = true
71:     isNull(C x xs) = false
72:   @-}

78: data L a where 
79:   N :: {v : L a | isNull v}
80:   C :: x:a -> xs:(L a) -> {v:(L a) | not (isNull v)}

Multiple measures for List

The types of data constructors will be the conjuction of all the inferred types:

92: data L a where 
93:   N :: {v : L a | (llen v) = 0}
94:   C :: a -> xs: L a -> {v:L a |(llen v) = 1 + (llen xs)}

99: data L a where 
100:   N :: {v : L a | isNull v}
101:   C :: a -> xs: L a -> {v:L a | not (isNull v)}

107: data L a where 
108:   N :: {v : L a | (llen v) = 0 && (isNull v)}
109:   C :: a -> xs: L a -> {v:L a |(llen v) = 1 + (llen xs) && not (isNull v)}

Invariants in Data Constructors

We can refine the definition of data types setting invariants

117: {-@ data L a = N
118:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}

124: data L a where
125:   N :: L a
126:   C :: x:a -> xs: L {v:a | x <= v} -> L a

• LiquidHaskell proves the property when C is called

• LiquidHaskell assumes the property when C is opened

Increasing Lists

This invariant constrains all Lists to increasing

142: {-@ data L a = N
143:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}

Insert sort

150: {-@ insert :: Ord a => a -> L a -> L a @-}
151: insert :: Ord a => a -> L a -> L a
152: forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert ay (x `C` xs) | {VV : a | (VV == x)}x x1:a
-> x2:a -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 <= x2))}<= {VV : a | (VV == y)}y    = {VV : a | (VV == x)}x x1:a
-> x2:(Measures.L {VV : a | (x1 <= VV)})
-> {x5 : (Measures.L a) | (((isNull x5)) <=> false) && ((llen x5) == (1 + (llen x2))) && ((x1 x5) == x1) && ((x2 x5) == x2)}`C` forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert {VV : a | (VV == y)}y {x2 : (Measures.L {VV : a | (x <= VV)}) | (x2 == xs)}xs
153:                     | otherwise = {VV : a | (VV == y)}y x1:a
-> x2:(Measures.L {VV : a | (x1 <= VV)})
-> {x5 : (Measures.L a) | (((isNull x5)) <=> false) && ((llen x5) == (1 + (llen x2))) && ((x1 x5) == x1) && ((x2 x5) == x2)}`C` forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert {VV : a | (VV == x)}x {x2 : (Measures.L {VV : a | (x <= VV)}) | (x2 == xs)}xs
154: 
155: {-@ insertSort  :: Ord a => [a] -> L a @-}
156: insertSort  :: Ord a => [a] -> L a
157: forall a. (GHC.Classes.Ord a) => [a] -> (Measures.L a)insertSort = (a -> (Measures.L a) -> (Measures.L a))
-> (Measures.L a) -> [a] -> (Measures.L a)foldr a -> (Measures.L a) -> (Measures.L a)insert {x3 : (Measures.L a) | (((isNull x3)) <=> true) && ((llen x3) == 0)}N

What if increasing and decreasing lists should co-exist?

We use abstract refinements to allow it!