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.

21: {-@ zero :: {v:Int | v = 0} @-}
22: zero     :: Int
23: {v : GHC.Types.Int | (v == 0)}zero     =  x1:GHC.Prim.Int# -> {x2 : GHC.Types.Int | (x2 == (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

57: type Nat = {v:Int | v >= 0}

And, via SMT based subtyping LiquidHaskell verifies:

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

Lists: Universal Invariants

Constructors enable universally quantified invariants.

For example, we define a list:

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

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

90: {-@ natList :: L Nat @-}
91: natList     :: L Int
92: (SimpleRefinements.L {v : GHC.Types.Int | (v >= 0)})natList     =  {x2 : GHC.Types.Int | (x2 == (0  :  int))}0 {x8 : GHC.Types.Int | (x8 >= 0)}
-> (SimpleRefinements.L {x8 : GHC.Types.Int | (x8 >= 0)})
-> (SimpleRefinements.L {x8 : GHC.Types.Int | (x8 >= 0)})`C` {x2 : GHC.Types.Int | (x2 == (1  :  int))}1 {x14 : GHC.Types.Int | (x14 /= 0) && (x14 > 0) && (x14 >= 0)}
-> (SimpleRefinements.L {x14 : GHC.Types.Int | (x14 /= 0) && (x14 > 0) && (x14 >= 0)})
-> (SimpleRefinements.L {x14 : GHC.Types.Int | (x14 /= 0) && (x14 > 0) && (x14 >= 0)})`C` {x2 : GHC.Types.Int | (x2 == (3  :  int))}3 {x14 : GHC.Types.Int | (x14 /= 0) && (x14 > 0) && (x14 >= 0)}
-> (SimpleRefinements.L {x14 : GHC.Types.Int | (x14 /= 0) && (x14 > 0) && (x14 >= 0)})
-> (SimpleRefinements.L {x14 : GHC.Types.Int | (x14 /= 0) && (x14 > 0) && (x14 >= 0)})`C` (SimpleRefinements.L {x2 : GHC.Types.Int | false})N

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

Refinement Function Types

Consider a safeDiv operator:

104: safeDiv    :: Int -> Int -> Int
105: GHC.Types.Int -> {v : GHC.Types.Int | (v /= 0)} -> GHC.Types.IntsafeDiv GHC.Types.Intx {v : GHC.Types.Int | (v /= 0)}y = {x2 : GHC.Types.Int | (x2 == x)}x x1:GHC.Types.Int
-> x2:GHC.Types.Int
-> {x6 : GHC.Types.Int | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x3 : GHC.Types.Int | (x3 == y) && (x3 /= 0)}y

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

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

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

Dependent Function Types

125: (!!)         :: L a -> Int -> a
126: (C x _)  !! 0 = x
127: (C _ xs) !! n = xs!!(n-1)
128: _        !! n = error "index too large"

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.