Simple Refinement Types

10: {-@ LIQUID "--no-termination" @-}
11: module SimpleRefinements where
12: import Language.Haskell.Liquid.Prelude
13: import Prelude hiding (abs, max)
14: 
15: -- boring haskell type sigs
16: zero    :: Int
17: zero'   :: Int
18: safeDiv :: Int -> Int -> Int
19: abs     :: Int -> Int
20: nats    :: L Int
21: evens   :: L Int
22: odds    :: L Int
23: range   :: Int -> Int -> L Int

Simple Refinement Types

Types + Predicates

Ex: `Int`egers equal to `0`

43: {-@ type EqZero = {v:Int | v = 0} @-}
44: 
45: {-@ zero :: EqZero @-}
46: {v : Int | (v == 0)}zero     =  x1:Int# -> {x2 : Int | (x2 == (x1  :  int))}0

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

Demo

Refinements Are Predicates

From A Decidable Logic

Expressions
Predicates

Expressions

78: e := x, y, z,...      -- variable
79:    | 0, 1, 2,...      -- constant
80:    | (e + e)          -- addition
81:    | (e - e)          -- subtraction
82:    | (c * e)          -- linear multiplication
83:    | (v e1 e2 ... en) -- uninterpreted function

Predicates

92: p := e           -- atom 
93:    | e1 == e2    -- equality
94:    | e1 <  e2    -- ordering 
95:    | (p && p)    -- and
96:    | (p || p)    -- or
97:    | (not p)     -- negation

Subtyping is Implication

PVS' Predicate Subtyping

Subtyping is Implication

If:	`P`	`=> Q`
Then:	`{v:t \| P}`	`<: {v:t \| Q}`

Example: Natural Numbers

143:         type Nat = {v:Int | 0 <= v}

By SMT:	`v = 0`	`=>` `0 <= v`
So:	`EqZero`	`<:` `Nat`

Hence, we can type:

165: {-@ zero' :: Nat @-}
166: {v : Int | (v >= 0)}zero'     =  {x3 : Int | (x3 == 0) && (x3 == SimpleRefinements.zero)}zero   -- zero :: EqZero <: Nat

Types = Universal Invariants

(Notoriously hard with pure SMT)

Types Yield Universal Invariants

Example: Lists

186: infixr `C`

191: data L a = N | C a (L a)

Every element in nats is non-negative:

202: {-@ nats :: L Nat @-}
203: (L {v : Int | (v >= 0)})nats     =  {x2 : Int | (x2 == (0  :  int))}0 {x8 : Int | (x8 >= 0)}
-> (L {x8 : Int | (x8 >= 0)}) -> (L {x8 : Int | (x8 >= 0)})`C` {x2 : Int | (x2 == (1  :  int))}1 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (3  :  int))}3 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` (L {x2 : Int | false})N

Demo: What if nats contained -2?

Example: Even/Odd Lists

220: {-@ type Even = {v:Int | v mod 2 =  0} @-}
221: {-@ type Odd  = {v:Int | v mod 2 /= 0} @-}

228: {-@ evens :: L Even @-}
229: (L {v : Int | ((v mod 2) == 0)})evens     =  {x2 : Int | (x2 == (0  :  int))}0 {x11 : Int | ((x11 mod 2) == 0) && (x11 >= 0)}
-> (L {x11 : Int | ((x11 mod 2) == 0) && (x11 >= 0)})
-> (L {x11 : Int | ((x11 mod 2) == 0) && (x11 >= 0)})`C` {x2 : Int | (x2 == (2  :  int))}2 {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)}
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})`C` {x2 : Int | (x2 == (4  :  int))}4 {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)}
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})`C` (L {x2 : Int | false})N
230: 
231: {-@ odds  :: L Odd  @-}
232: (L {v : Int | ((v mod 2) == 1)})odds      =  {x2 : Int | (x2 == (1  :  int))}1 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (3  :  int))}3 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (5  :  int))}5 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` (L {x2 : Int | false})N

Demo: What if evens contained 1?

Contracts: Function Types

Example: `safeDiv`

Precondition divisor is non-zero.

263: {-@ type NonZero = {v:Int | v /= 0} @-}

Example: `safeDiv`

Pre-condition divisor is non-zero.
Input type specifies pre-condition

280: {-@ safeDiv :: Int -> NonZero -> Int @-}
281: Int -> {v : Int | (v /= 0)} -> IntsafeDiv Intx {v : Int | (v /= 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

304: {-@ abs       :: x:Int -> Nat @-}
305: Int -> {v : Int | (v >= 0)}abs Intx 
306:   | {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 
307:   | otherwise = {x2 : Int | (x2 == (0  :  int))}0 x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == x)}x

Dependent Function Types

Outputs refer to inputs

Relational invariants

Dependent Function Types

Example: `range`

(range i j) returns Ints between i and j

Example: `range`

(range i j) returns Ints between i and j

343: {-@ type Btwn I J = {v:_ | (I<=v && v<J)} @-}

Example: `range`

(range i j) returns Ints between i and j

355: {-@ range :: i:Int -> j:Int -> L (Btwn i j) @-}
356: x1:Int -> x2:Int -> (L {v : Int | (v < x2) && (x1 <= v)})range Inti Intj            = 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
357:   where
358:     x1:{VV : Int | (VV >= i) && (i <= VV)}
-> (L {VV : Int | (VV >= i) && (VV >= x1) && (VV < j) && (i <= VV) && (x1 <= VV)})go {VV : Int | (VV >= i) && (i <= VV)}n | {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` x1:{VV : Int | (VV >= i) && (i <= VV)}
-> (L {VV : Int | (VV >= i) && (VV >= x1) && (VV < j) && (i <= VV) && (x1 <= 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)  
359:          | otherwise =  (L {x2 : Int | false})N

Note: Type of go is automatically inferred

Example: Indexing Into List

373: (!)          :: L a -> Int -> a
374: (C x _)  forall a. (L a) -> Int -> a! 0 = {VV : a | (VV == x)}x
375: (C _ xs) ! i = (L a)xs forall a. (L a) -> Int -> a! (Inti x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == (1  :  int))}1)
376: _        ! _ = {x1 : [Char] | false} -> aliquidError {x2 : [Char] | ((len x2) >= 0)}"Oops!"

(Mouseover to view type of liquidError)

To ensure safety, require i between 0 and list length

Need way to measure the length of a list [continue...]