Abstract Refinements

Example: plus

25: {-@ plus :: x:_ -> y:_ -> {v:_ | v=x+y} @-}
26: x1:Int -> x2:Int -> {v : Int | (v == (x1 + x2))}plus Intx Inty = {x2 : Int | (x2 == x)}x x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == y)}y

Example: plus 3

36: {-@ plus3' :: x:Int -> {v:Int | v = x + 3} @-}
37: x1:Int -> {v : Int | (v == (x1 + 3))}plus3'     = x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}plus {x2 : Int | (x2 == (3  :  int))}3

Easily verified by LiquidHaskell

A Composed Variant

Lets define plus3 by composition

A Composition Operator

53: (#) :: (b -> c) -> (a -> b) -> a -> c
54: forall a b c. (a -> b) -> (c -> a) -> c -> b(#) a -> bf a -> bg ax = a -> bf (a -> bg {VV : a | (VV == x)}x)

plus3 By Composition

62: {-@ plus3'' :: x:Int -> {v:Int | v = x + 3} @-}
63: x1:Int -> {v : Int | (v == (x1 + 3))}plus3''     = x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}plus {x2 : Int | (x2 == (1  :  int))}1 (Int -> Int) -> (Int -> Int) -> Int -> Int# x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}plus {x2 : Int | (x2 == (2  :  int))}2

Yikes! Verification fails. But why?

How to type compose (#) ?

This specification is too weak

80: (#) :: (b -> c) -> (a -> b) -> (a -> c)

Output type does not relate c with a!

How to type compose (.) ?

Write specification with abstract refinement type:

95: {-@ (.) :: forall <p :: b->c->Prop, 
96:                    q :: a->b->Prop>.
97:              f:(x:b -> c<p x>) 
98:           -> g:(x:a -> b<q x>) 
99:           -> y:a -> exists[z:b<q y>].c<p z>
100:  @-}
101: forall a b c <p :: b-> a-> Bool, q :: c-> b-> Bool>.
(x2:b -> {VV : a<p x2> | true})
-> (x4:c -> {VV : b<q x4> | true})
-> x5:c
-> exists [z:{VV : b<q x5> | true}].{VV : a<p z> | true}(.) x1:a -> {VV : b | ((papp2 p VV x1))}f x1:a -> {VV : b | ((papp2 q VV x1))}g ay = x1:a -> {VV : b | ((papp2 p VV x1))}f (x1:a -> {VV : b | ((papp2 q VV x1))}g {VV : a | (VV == y)}y)

Using (.) Operator

110: {-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-}
111: x1:Int -> {v : Int | (v == (x1 + 3))}plus3     = x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}plus {x2 : Int | (x2 == (1  :  int))}1 forall <q :: GHC.Types.Int-> GHC.Types.Int-> Bool, p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
(x2:Int -> {x6 : Int<p x2> | true})
-> (x4:Int -> {x7 : Int<q x4> | true})
-> x5:Int
-> exists [z:{x7 : Int<q x5> | true}].{x6 : Int<p z> | true}. x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}plus {x2 : Int | (x2 == (2  :  int))}2

Using (.) Operator

123: {-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-}
124: plus3     = plus 1 . plus 2

LiquidHaskell instantiates

• p with \x -> v = x + 1
• q with \x -> v = x + 2

Using (.) Operator

138: {-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-}
139: plus3     = plus 1 . plus 2

To infer that output of plus3 has type:

exists [z:{v = y + 2}].{v = z + 1}

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Strengthened Constructors
4. Abstract: Refinements over Type Signatures
   • Dependencies using refinement parameters