LiquidHaskell *strengthens* data constructor types

74: data L a where 
75:   N :: {v: L a | (llen v) = 0}
76:   C :: a -> xs:L a 
77:          -> {v:L a | (llen v) = 1 + (llen xs)}

Measures Are Uninterpreted --------------------------

85: data L a where 
86:   N :: {v: L a | (llen v) = 0}
87:   C :: a -> xs:L a 
88:          -> {v:L a | (llen v) = 1 + (llen xs)}

`llen` is an *uninterpreted function* in SMT logic Measures Are Uninterpreted -------------------------- In SMT, [uninterpreted function](http://fm.csl.sri.com/SSFT12/smt-euf-arithmetic.pdf) `f` obeys *congruence* axiom: `forall x y. (x = y) => (f x) = (f y)`

All other facts about `llen` asserted at *fold* and *unfold*

Measures Are Uninterpreted -------------------------- All other facts about `llen` asserted at *fold* and *unfold*

**Fold**

117: z = C x y -- z :: {v | llen v = 1 + llen y}

**Unfold**

125: case z of 
126:   N     -> e1 -- z :: {v | llen v = 0}
127:   C x y -> e2 -- z :: {v | llen v = 1 + llen y}

Measured Refinements -------------------- Now, we can verify:

140: {-@ length      :: xs:L a -> (EqLen xs) @-}
141: forall a. x1:(L a) -> {VV : (Int) | (VV == (llen x1)) && (VV >= 0)}length N        = x1:(Int#) -> {x2 : (Int) | (x2 == (x1  :  int))}0
142: length (C _ xs) = {x2 : (Int) | (x2 == (1  :  int))}1 x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ (forall a. x1:(L a) -> {VV : (Int) | (VV == (llen x1)) && (VV >= 0)}length {x2 : (L a) | (x2 == xs)}xs)

Where `EqLen` is a type alias:

152: {-@ type EqLen Xs = {v:Nat | v = (llen Xs)} @-}

List Indexing Redux ------------------- We can type list indexed lookup:

165: {-@ (!)      :: xs:L a -> (LtLen xs) -> a @-}
166: (C x _)  forall a.
x1:(L a) -> {VV : (Int) | (VV >= 0) && (VV < (llen x1))} -> a! 0 = {VV : a | (VV == x)}x
167: (C _ xs) ! i = (L {VV : a | (x <= VV)})xs forall a.
x1:(L a) -> {VV : (Int) | (VV >= 0) && (VV < (llen x1))} -> a! ({x2 : (Int) | (x2 >= 0)}i x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}- {x2 : (Int) | (x2 == (1  :  int))}1)
168: _        ! _ = {x1 : [(Char)] | false} -> {VV : a | false}liquidError {x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}"never happens!"

Where `LtLen` is a type alias:

176: {-@ type LtLen Xs = {v:Nat | v < (llen Xs)} @-}

List Indexing Redux ------------------- Now we can type list indexed lookup:

186: {-@ (!)      :: xs:L a -> (LtLen xs) -> a @-}
187: (C x _)  ! 0 = x
188: (C _ xs) ! i = xs ! (i - 1)
189: _        ! _ = liquidError "never happens!"

Demo: What if we *remove* the precondition? Multiple Measures ----------------- LiquidHaskell allows *many* measures for a type Multiple Measures ----------------- **Example:** Nullity of a `List`

209: {-@ measure isNull :: (L a) -> Prop
210:     isNull (N)      = true
211:     isNull (C x xs) = false           @-}

LiquidHaskell **strengthens** data constructors

219: data L a where 
220:   N :: {v : L a | (isNull v)}
221:   C :: a -> L a -> {v:(L a) | not (isNull v)}

Multiple Measures ----------------- LiquidHaskell *conjoins* data constructor types:

232: data L a where 
233:   N :: {v:L a |  (llen v) = 0 
234:               && (isNull v) }
235:   C :: a 
236:     -> xs:L a 
237:     -> {v:L a |  (llen v) = 1 + (llen xs) 
238:               && not (isNull v)          }

Multiple Measures ----------------- Unlike [indexed types](http://dl.acm.org/citation.cfm?id=270793) ...
+

Measures *decouple* properties from structures

Support *multiple* properties over structures

Enable *reuse* of structures

Invaluable in practice!

Refined Data Constructors ------------------------- Can *directly pack* properties inside data constructors

266: {-@ data L a = N
267:              | C (x :: a) 
268:                  (xs :: L {v:a | x <= v})  @-}

Specifies *increasing* Lists

Refined Data Constructors ------------------------- **Example:** Increasing Lists, with strengthened constructors:

286: data L a where
287:   N :: L a
288:   C :: x:a -> xs: L {v:a | x <= v} -> L a

LiquidHaskell *checks* property when *folding* `C`

LiquidHaskell *assumes* property when *unfolding* `C`

Refined Data Constructors ------------------------- Demo: Insertion Sort (hover for inferred types)

302: forall a. (Ord a) => [a] -> (L a)insertSort = (a -> (L a) -> (L a)) -> (L a) -> [a] -> (L a)foldr a -> (L a) -> (L a)insert {x3 : (L {VV : a | false}) | (((isNull x3)) <=> true) && ((llen x3) == 0)}N
303: 
304: forall a. (Ord a) => a -> (L a) -> (L a)insert ay (x `C` xs) 
305:   | {VV : a | (VV == y)}y x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}<= {VV : a | (VV == x)}x    = {VV : a | (VV == y)}y x1:{VV : a | (VV >= y)}
-> x2:(L {VV : a | (VV >= y) && (x1 <= VV)})
-> {x3 : (L {VV : a | (VV >= y)}) | (((isNull x3)) <=> false) && ((llen x3) == (1 + (llen x2)))}`C` ({VV : a | (VV == x)}x x1:{VV : a | (VV >= x) && (VV >= y)}
-> x2:(L {VV : a | (VV >= x) && (VV >= y) && (x1 <= VV)})
-> {x3 : (L {VV : a | (VV >= x) && (VV >= y)}) | (((isNull x3)) <=> false) && ((llen x3) == (1 + (llen x2)))}`C` {x2 : (L {VV : a | (x <= VV)}) | (x2 == xs)}xs)
306:   | otherwise = {VV : a | (VV == x)}x x1:{VV : a | (VV >= x)}
-> x2:(L {VV : a | (VV >= x) && (x1 <= VV)})
-> {x3 : (L {VV : a | (VV >= x)}) | (((isNull x3)) <=> false) && ((llen x3) == (1 + (llen x2)))}`C` forall a. (Ord a) => a -> (L a) -> (L a)insert {VV : a | (VV == y)}y {x2 : (L {VV : a | (x <= VV)}) | (x2 == xs)}xs
307: insert y N    = {VV : a | (VV == y)}y x1:{VV : a | (VV == y)}
-> x2:(L {VV : a | (VV == y) && (x1 <= VV)})
-> {x3 : (L {VV : a | (VV == y)}) | (((isNull x3)) <=> false) && ((llen x3) == (1 + (llen x2)))}`C` {x3 : (L {VV : a | false}) | (((isNull x3)) <=> true) && ((llen x3) == 0)}N

**Problem 1:** What if we need *both* [increasing and decreasing lists](http://web.cecs.pdx.edu/~sheard/Code/QSort.html)?

Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3.

**Measures:** Strengthened Constructors

*Decouple* structure & property, enable *reuse*