# Simple Refinement Types

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

# Simple Refinement Types

This type describes `Int` values that equal `0`.

```20: {-@ zero :: {v:Int | v = 0} @-}
21: zero     :: Int
22: {VV : (GHC.Types.Int) | (VV == 0)}zero     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0
```

# Refinements are logical formulas

Since

• `v = 0` implies `v >= 0`

Therefore

• `{v:Int | v = 0} <: {v:Int | v >= 0}`

# Refinements are logical formulas

So we can have a type for natural numbers:
```41: type Nat = {v:Int | v >= 0}
```

And we can type `0` as `Nat`:

```51: {-@ zero' :: Nat @-}
52: zero'     :: Int
53: {VV : (GHC.Types.Int) | (VV >= 0)}zero'     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0
```

# Refinements are logical formulas

Similarly, since

• `v = 0 => v mod 2 = 0`

Therefore

• `{v:Int | v = 0} <: {v:Int | v mod 2 = 0}`

Thus, via SMT based subtyping LiquidHaskell verifies:

```70: {-@ type Even = {v:Int | v mod 2 = 0} @-}
71:
72: {-@ zero'' :: Even @-}
73: zero''     :: Int
74: {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}zero''     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0
```

# Lists

Refinements can live inside type constructors:

```84: infixr `C`
85: data L a = N | C a (L a)
```

# Lists: Universal Invariants

Constructors enable universally quantified invariants.

For example, every element in a list is non-negative:

```96: {-@ natList :: L Nat @-}
97: natList     :: L Int
98: (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})natList     =  {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= zero)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= zero)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= zero)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (3  :  int))}3 {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | false}) | ((llen VV) == 0)}N
```

or, every element in a list is even:

```104: {-@ evenList :: L Even @-}
105: evenList     :: L Int
106: (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})evenList     =  {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV >= 0) && (VV >= zero)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV >= 0) && (VV >= zero)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV >= 0) && (VV >= zero)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (2  :  int))}2 {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (8  :  int))}8 {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | false}) | ((llen VV) == 0)}N
```

Demo: Lets see what happens if `evenList` contained an odd number.

# Refinement Function Types

Consider a `safeDiv` operator:

```119: safeDiv    :: Int -> Int -> Int
120: (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV /= 0)} -> (GHC.Types.Int)safeDiv (GHC.Types.Int)x {VV : (GHC.Types.Int) | (VV /= 0)}y = {VV : (GHC.Types.Int) | (VV == x)}x x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x / y))}`div` {VV : (GHC.Types.Int) | (VV == y) && (VV /= 0)}y
```

We can use refinements to specify a precondition: divisor is non-zero

```126: {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-}
```

Demo: Lets see what happens if we make `safeDiv`ision by zero.

# Dependent Function Types

Consider a list indexing function:
```137: (!!)         :: L a -> Int -> a
138: (C x _) !! 0 = x
139: (C _ xs)!! n = xs!!(n-1)
140: _       !! _ = liquidError "This should not happen!"
```

We desire precondition that index `i` be between `0` and list length.

# Measuring A List's length in logic

We define a measure for the length of a `List`

```153: {-@ measure llen :: (L a) -> Int
154:     llen(N)      = 0
155:     llen(C x xs) = 1 + (llen xs)
156:   @-}
```

The measure strengthens the type of data constructors
```162: data L a where
163:   N :: {v : L a | (llen v) = 0}
164:   C :: a -> xs:(L a) -> {v:(L a) |(llen v) = 1 + (llen xs)}
```

# Measuring A List's length in logic

Now we can verify

```175: {-@ length :: xs:(L a) -> {v:Int | v = (llen xs)} @-}
176: length     :: L a -> Int
177: forall a.
xs:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length N        = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0
178: length (C _ xs) = {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ (xs:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L a) | (VV == xs)}xs)
```

# Measuring A List's length in logic

And we can type `(!!)` as

```189: {-@ (!!) :: ls:(L a) -> {v:Nat | v < (llen ls)} -> a @-}
190: (!!)         :: L a -> Int -> a
191: (C x _) forall a.
ls:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))} -> a!! 0 = {VV : a | (VV == x)}x
192: (C _ xs)!! n = (SimpleRefinements.L a)xsls:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))} -> a!!({VV : (GHC.Types.Int) | (VV >= 0)}nx:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x - y))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
193: _       !! _ = {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