Simple Refinement Types

```7: module SimpleRefinements where
```

Simple Refinement Types

We use special comments to give specifications, as refinement types.

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

```22: {-@ zero :: {v:Int | v = 0} @-}
23: zero     :: Int
24: {VV : (GHC.Types.Int) | (VV == 0)}zero     =  x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1  :  int))}0
```

Refinements are logical formulas

If

• refinement of `T1` implies refinement of `T2`

• `p1 => p2`

Then

• `T1` is a subtype of `T2`

• `{v:t | p1} <: {v:t | p2}`

Refinements are logical formulas

For example, 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:
```58: type Nat = {v:Int | v >= 0}
```

And, via SMT based subtyping LiquidHaskell verifies:

```68: {-@ zero' :: Nat @-}
69: zero'     :: Int
70: {VV : (GHC.Types.Int) | (VV >= 0)}zero'     =  x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1  :  int))}0
```

Lists: Universal Invariants

Constructors enable universally quantified invariants.

For example, we define a list:

```82: infixr `C`
83: data L a = N | C a (L a)
```

And specify that, every element in a list is non-negative:

```91: {-@ natList :: L Nat @-}
92: natList     :: L Int
93: (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})natList     =  {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= SimpleRefinements.zero)}
-> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= SimpleRefinements.zero)})
-> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= SimpleRefinements.zero)})`C` {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)}
-> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)})
-> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)})`C` {VV : (GHC.Types.Int) | (VV == (3  :  int))}3 {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)}
-> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)})
-> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)})`C` (SimpleRefinements.L {VV : (GHC.Types.Int) | false})N
```

Demo: Lets see what happens if `natList` contained a negative number.

Refinement Function Types

Consider a `safeDiv` operator:

```105: safeDiv    :: Int -> Int -> Int
106: (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 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (((x1 >= 0) && (x2 >= 0)) => (VV >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (VV <= x1)) && (VV == (x1 / x2))}`div` {VV : (GHC.Types.Int) | (VV == y) && (VV /= 0)}y
```

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

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

Demo: Lets see what happens if the preconditions cannot be proven.

Dependent Function Types

Consider a list indexing function:
```126: (!!)         :: L a -> Int -> a
127: (C x _) !! 0 = x
128: (C _ xs)!! n = xs!!(n-1)
129: _       !! _ = liquidError "This should not happen!"
```

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

We use measures to talk about the length of a list in logic.