Measures

7: module Measures where
8: import Prelude hiding ((!!), length)
9: import Language.Haskell.Liquid.Prelude

Measuring A List's length in logic

On List data type

18: infixr `C`
19: data L a = N | C a (L a)

We define a measure for the length of a List

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

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

Measuring A List's length in logic

Now we can verify

47: {-@ length :: xs:(L a) -> {v:Int | v = (llen xs)} @-}
48: length     :: L a -> Int
49: forall a.
x1:(Measures.L a) -> {VV : (GHC.Types.Int) | (VV == (llen x1))}length N        = x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1  :  int))}0
50: length (C _ xs) = {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ (forall a.
x1:(Measures.L a) -> {VV : (GHC.Types.Int) | (VV == (llen x1))}length {VV : (Measures.L a) | (VV == xs)}xs)

Measuring A List's length in logic

And we can type (!!) as

62: {-@ (!!)     :: ls:(L a) -> i:{v:Nat | v < (llen ls)} -> a @-}
63: (!!)         :: L a -> Int -> a
64: (C x _) forall a.
x1:(Measures.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen x1))} -> a!! 0 = {VV : a | (VV == x)}x
65: (C _ xs)!! n = (Measures.L {VV : a | (x <= VV)})xsforall a.
x1:(Measures.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen x1))} -> a!!({VV : (GHC.Types.Int) | (VV >= 0)}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
66: _       !! _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}liquidError {VV : [(GHC.Types.Char)] | ((len VV) >= 0) && ((sumLens VV) >= 0)}"This should not happen!"

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

81: {-@ measure isNull :: (L a) -> Prop
82:     isNull(N)      = true
83:     isNull(C x xs) = false
84:   @-}

90: data L a where 
91:   N :: {v : L a | isNull v}
92:   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:

104: data L a where 
105:   N :: {v : L a | (llen v) = 0}
106:   C :: a -> xs: L a -> {v:L a |(llen v) = 1 + (llen xs)}

111: data L a where 
112:   N :: {v : L a | isNull v}
113:   C :: a -> xs: L a -> {v:L a | not (isNull v)}

119: data L a where 
120:   N :: {v : L a | (llen v) = 0 && (isNull v)}
121:   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

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

137: data L a where
138:   N :: L a
139:   C :: x:a -> xs: L {v:a | x <= v} -> L a

LiquidHaskell

• Proves the property when C is called

• Assumes the property when C is opened

Increasing Lists

This invariant constrains all Lists to increasing

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

Insert sort

163: {-@ insert :: Ord a => a -> L a -> L a @-}
164: insert :: Ord a => a -> L a -> L a
165: 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 -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | (VV == y)}y    = {VV : a | (VV == x)}x x1:{VV : a | (VV >= x)}
-> x2:(Measures.L {VV : a | (VV >= x) && (x1 <= VV)})
-> {VV : (Measures.L {VV : a | (VV >= x)}) | (((isNull VV)) <=> false) && ((llen VV) == (1 + (llen x2)))}`C` forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert {VV : a | (VV == y)}y {VV : (Measures.L {VV : a | (x <= VV)}) | (VV == xs)}xs
166:                     | otherwise = {VV : a | (VV == y)}y x1:{VV : a | (VV >= y)}
-> x2:(Measures.L {VV : a | (VV >= y) && (x1 <= VV)})
-> {VV : (Measures.L {VV : a | (VV >= y)}) | (((isNull VV)) <=> false) && ((llen VV) == (1 + (llen x2)))}`C` forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert {VV : a | (VV == x)}x {VV : (Measures.L {VV : a | (x <= VV)}) | (VV == xs)}xs
167: 
168: {-@ insertSort  :: Ord a => [a] -> L a @-}
169: insertSort  :: Ord a => [a] -> L a
170: 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 {VV : (Measures.L {VV : a | false}) | (((isNull VV)) <=> true) && ((llen VV) == 0)}N

What if increasing and decreasing lists should co-exist?

We use abstract refinements to allow it!