# Measures

```7: module Measures where
8: import Prelude hiding ((!!), length)
```

# 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:   @-}
```

LiquidHaskell then automatically strengthens the types of data constructors
```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

```48: {-@ length :: xs:(L a) -> {v:Int | v = (llen xs)} @-}
49: length     :: L a -> Int
50: 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
51: length (C _ ys) = {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 == ys)}ys)
```

# Measuring A List's length in logic

And we can type `(!!)` as

```63: {-@ (!!) :: ls:(L a) -> {v:Nat | v < (llen ls)} -> a @-}
64: (!!)         :: L a -> Int -> a
65: (C x _) forall a.
x1:(Measures.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen x1))} -> a!! 0 = {VV : a | (VV == x)}x
66: (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)
67: _       !! _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}liquidError {VV : [(GHC.Types.Char)] | ((len 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`

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

LiquidHaskell then automatically strengthens the types of data constructors
```91: data L a where
92:   N :: {v : L a | isNull v}
93:   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:

The types from `llen` definition
```105: data L a where
106:   N :: {v : L a | (llen v) = 0}
107:   C :: a -> xs: L a -> {v:L a |(llen v) = 1 + (llen xs)}
```

and the types from `isNull`
```112: data L a where
113:   N :: {v : L a | isNull v}
114:   C :: a -> xs: L a -> {v:L a | not (isNull v)}
```

So, the final types will be
```120: data L a where
121:   N :: {v : L a | (llen v) = 0 && (isNull v)}
122:   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

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

As before,the types of data constuctors are weakened to
```138: data L a where
139:   N :: L a
140:   C :: x:a -> xs: L {v:a | x <= v} -> L a
```

# Invariants in Data Constructors

We can refine the definition of data types setting invariants

```149: {-@ data L a = N
150:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}
```

As before,the types of data constuctors are strengthened to
```156: data L a where
157:   N :: L a
158:   C :: x:a -> xs: L {v:a | x <= v} -> L a
```

• Proves the property when `C` is called

• Assumes the property when `C` is opened

# Increasing Lists

This invariant constrains all Lists to increasing

```174: {-@ data L a = N
175:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}
```
```182: {-@ insert :: Ord a => a -> L a -> L a @-}
183: insert :: Ord a => a -> L a -> L a
184: 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
185:                     | 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
186:
187: {-@ insertSort  :: Ord a => [a] -> L a @-}
188: insertSort  :: Ord a => [a] -> L a
189: 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?

# Invariants in ByteString

Invariants on the definition of Bytestring:
```199: measure fplen :: ForeignPtr a -> Int
200:
201: data ByteString = PS
202:   { pay :: ForeignPtr Word8
203:   , off :: {v:Nat | v <= (fplen pay)}
204:   , len :: {v:Nat | off + v <= (fplen pay)} }
```

Allow us to enforce low-level memory safety.