{#simplerefinements} ======================= Simple Refinement Types ----------------------- Simple Refinement Types ======================= Types + Predicates ------------------ Example ------- Integers equal to `0` 
45: {-@ type EqZero = {v:Int | v = 0} @-}
Example ------- Integers equal to `0` 
57: {-@ zero :: EqZero @-}
58: {VV : (Int) | (VV == 0)}zero     =  x1:(Int#) -> {x2 : (Int) | (x2 == (x1  :  int))}0

Refinement types via special comments `{-@ ... @-}`

Demo Lets take a look.
{#refinementsArePredicates} ============================ Refinements Are Predicates -------------------------- Refinements Are Predicates ========================== Subtyping is Implication ------------------------ [Predicate Subtyping](http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf) Subtyping is Implication ------------------------
-------- --- --------------------------------------------- **If** : Refinement of `S` *implies* refinement of `T` **Then** : `S` is a *subtype* of `T` -------- --- ---------------------------------------------
Subtyping is Implication ------------------------
-------- --- ---------------------------- **If** : `p => q` **Then** : `{v : t | p} <: {v : t | q}` -------- --- ---------------------------- Subtyping is Implication ------------------------
-------- --- --------------------------------------------------- **As** : `v=0` *implies* `0<=v` ... via SMT **So** : `{v:Int | v=0} <: {v:Int | 0<=v}` -------- --- --------------------------------------------------- Example: Natural Numbers ------------------------ . 
134: type Nat = {v : Int | 0 <= v}

Via SMT, LiquidHaskell infers `EqZero <: Nat`, hence: 
144: {-@ zero' :: Nat @-}
145: {VV : (Int) | (VV >= 0)}zero'     =  {x3 : (Int) | (x3 == 0) && (x3 == SimpleRefinements.zero)}zero
{#universalinvariants} ======================= Types = Universal Invariants ---------------------------- (Notoriously hard with *pure* SMT) Types Yield Universal Invariants ================================ Example: Lists -------------- 
169: data L a = N | C a (L a)

*Every element* in `nats` is non-negative: 
177: {-@ nats :: L Nat @-}
178: (L {VV : (Int) | (VV >= 0)})nats     =  {x2 : (Int) | (x2 == (0  :  int))}0 {x14 : (Int) | (x14 >= 0) && (x14 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x14)}
-> (L {x14 : (Int) | (x14 >= 0) && (x14 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x14)})
-> (L {x14 : (Int) | (x14 >= 0) && (x14 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x14)})`C` {x2 : (Int) | (x2 == (1  :  int))}1 {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})`C` {x2 : (Int) | (x2 == (3  :  int))}3 {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})`C` (L {x2 : (Int) | false})N

Demo: What if `nats` contained `-2`?
Example: Even/Odd Lists ----------------------- 
195: {-@ type Even = {v:Int | v mod 2 =  0} @-}
196: {-@ type Odd  = {v:Int | v mod 2 /= 0} @-}


203: {-@ evens :: L Even @-}
204: (L {VV : (Int) | ((VV mod 2) == 0)})evens     =  {x2 : (Int) | (x2 == (0  :  int))}0 {x17 : (Int) | ((x17 mod 2) == 0) && (x17 >= 0) && (x17 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x17)}
-> (L {x17 : (Int) | ((x17 mod 2) == 0) && (x17 >= 0) && (x17 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x17)})
-> (L {x17 : (Int) | ((x17 mod 2) == 0) && (x17 >= 0) && (x17 >= SimpleRefinements.zero) && (SimpleRefinements.zero <= x17)})`C` {x2 : (Int) | (x2 == (2  :  int))}2 {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)}
-> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)})
-> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)})`C` {x2 : (Int) | (x2 == (4  :  int))}4 {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)}
-> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)})
-> (L {x23 : (Int) | ((x23 mod 2) == 0) && (x23 /= 0) && (x23 > 0) && (x23 > SimpleRefinements.zero) && (x23 >= 0) && (SimpleRefinements.zero <= x23)})`C` (L {x2 : (Int) | false})N
205: 
206: {-@ odds  :: L Odd  @-}
207: (L {VV : (Int) | ((VV mod 2) == 1)})odds      =  {x2 : (Int) | (x2 == (1  :  int))}1 {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})`C` {x2 : (Int) | (x2 == (3  :  int))}3 {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})`C` {x2 : (Int) | (x2 == (5  :  int))}5 {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)}
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})
-> (L {x20 : (Int) | ((x20 mod 2) == 1) && (x20 > 0) && (x20 > SimpleRefinements.zero) && (x20 >= 0) && (SimpleRefinements.zero <= x20)})`C` (L {x2 : (Int) | false})N
Demo: What if `evens` contained `1`?
{#functiontypes} ================= Contracts = Function Types -------------------------- Contracts: Function Types ========================= Example: `safeDiv` ------------------
**Precondition** divisor is *non-zero*. 
237: {-@ type NonZero = {v:Int | v /= 0} @-}

Example: `safeDiv` ------------------
+ **Pre-condition** divisor is *non-zero*. + **Input type** specifies *pre-condition* 
254: {-@ safeDiv :: Int -> NonZero -> Int @-}
255: (Int) -> {VV : (Int) | (VV /= 0)} -> (Int)safeDiv (Int)x {VV : (Int) | (VV /= 0)}y = {x2 : (Int) | (x2 == x)}x x1:(Int)
-> x2:(Int)
-> {x6 : (Int) | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x3 : (Int) | (x3 == y) && (x3 /= 0)}y

Demo: What if precondition does not hold?
Example: `abs` --------------
+ **Postcondition** result is non-negative + **Output type** specifies *post-condition* 
278: {-@ abs       :: x:Int -> Nat @-}
279: (Int) -> {VV : (Int) | (VV >= 0)}abs (Int)x 
280:   | {x2 : (Int) | (x2 == (0  :  int))}0 x1:(Int)
-> x2:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}<= {x2 : (Int) | (x2 == x)}x    = {x2 : (Int) | (x2 == x)}x 
281:   | otherwise = {x2 : (Int) | (x2 == (0  :  int))}0 x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}- {x2 : (Int) | (x2 == x)}x
{#dependentfunctions} ====================== Dependent Function Types ------------------------ + Outputs *refer to* inputs + *Relational* invariants Dependent Function Types ======================== Example: `range` ---------------- `(range i j)` returns `Int`s between `i` and `j` Example: `range` ---------------- `(range i j)` returns `Int`s between `i` and `j` 
313: {-@ type Btwn I J = {v:_|(I <= v && v < J)} @-}
Example: `range` ---------------- `(range i j)` returns `Int`s between `i` and `j` 
324: {-@ range :: i:Int -> j:Int -> L (Btwn i j) @-}
325: i:(Int) -> j:(Int) -> (L {v : (Int) | (v < j) && (i <= v)})range (Int)i (Int)j         = x1:{x10 : (Int) | (x10 >= i) && (i <= x10)}
-> (L {x7 : (Int) | (x7 >= i) && (x7 >= x1) && (x7 < j) && (i <= x7) && (x1 <= x7)})go {x2 : (Int) | (x2 == i)}i
326:   where
327:     n:{VV : (Int) | (VV >= i) && (i <= VV)}
-> (L {VV : (Int) | (VV >= i) && (VV >= n) && (VV < j) && (i <= VV) && (n <= VV)})go {VV : (Int) | (VV >= i) && (i <= VV)}n
328:       | {x4 : (Int) | (x4 == n) && (x4 >= i) && (i <= x4)}n x1:(Int) -> x2:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}< {x2 : (Int) | (x2 == j)}j     = {x4 : (Int) | (x4 == n) && (x4 >= i) && (i <= x4)}n {x20 : (Int) | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)}
-> (L {x20 : (Int) | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})
-> (L {x20 : (Int) | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})`C` n:{VV : (Int) | (VV >= i) && (i <= VV)}
-> (L {VV : (Int) | (VV >= i) && (VV >= n) && (VV < j) && (i <= VV) && (n <= VV)})go ({x4 : (Int) | (x4 == n) && (x4 >= i) && (i <= x4)}n x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {x2 : (Int) | (x2 == (1  :  int))}1)  
329:       | otherwise = (L {x2 : (Int) | false})N

**Question:** What is the type of `go` ?
Example: Indexing Into List --------------------------- 
343: (!)          :: L a -> Int -> a
344: (C x _)  forall a. (L a) -> (Int) -> a! 0 = {VV : a | (VV == x)}x
345: (C _ xs) ! i = (L a)xs (L a) -> (Int) -> a! ((Int)i x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}- {x2 : (Int) | (x2 == (1  :  int))}1)
346: _        ! _ = {x1 : [(Char)] | false} -> {VV : a | false}liquidError {x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}"Oops!"

(Mouseover to view type of `liquidError`)

-
**Q:** How to ensure safety?
-
**A:** Precondition: `i` between `0` and list **length**.
Need way to [measure](#measures) *length of a list* ...