Abstract Refinements

Very General Mechanism

Next: Lets add parameters...

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?


(Hover mouse over # for a clue)

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


Verifies!

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}

<:

{v:Int|v=3}

Recap

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