Abstract Refinements {#composition} =================================== Very General Mechanism ---------------------- **Next:** Lets add parameters...

11: module Composition where
12: 
13: import Prelude hiding ((.))
14: 
15: plus     :: Int -> Int -> Int
16: plus3'   :: Int -> Int

Example: `plus` ---------------

25: {-@ plus :: x:_ -> y:_ -> {v:_ | v=x+y} @-}
26: x:(Int) -> y:(Int) -> {v : (Int) | (v == (x + y))}plus (Int)x (Int)y = {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: x:(Int) -> {VV : (Int) | (VV == (x + 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: x:(Int) -> {VV : (Int) | (VV == (x + 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>.
(x:b -> {VV : a<p x> | true})
-> (x:c -> {VV : b<q x> | true})
-> y:c
-> exists [z:{VV : b<q y> | true}].{VV : a<p z> | true}(.) x:a -> {VV : b | ((papp2 p VV x))}f x:a -> {VV : b | ((papp2 q VV x))}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: x:(Int) -> {VV : (Int) | (VV == (x + 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>.
(x:(Int) -> {x8 : (Int)<p x> | true})
-> (x:(Int) -> {x9 : (Int)<q x> | true})
-> x3:(Int)
-> exists [z:{x9 : (Int)<q x3> | true}].{x8 : (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