7: module Composition where
Consider a simple plus
function
16: {-@ plus :: x:Int -> y:Int -> {v:Int | v = x + y} @-} 17: plus :: Int -> Int -> Int 18: x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}plus (GHC.Types.Int)x (GHC.Types.Int)y = {VV : (GHC.Types.Int) | (VV == x)}x x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == y)}y
Consider a simple use of plus
a function that adds 3
to its input:
27: {-@ plus3' :: x:Int -> {v:Int | v = x + 3} @-} 28: plus3' :: Int -> Int 29: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + 3))}plus3' (GHC.Types.Int)x = {VV : (GHC.Types.Int) | (VV == x)}x x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (3 : int))}3
The refinement type captures its behaviour...
... and LiquidHaskell easily verifies this type.
Instead, suppose we defined the previous function by composition
We first add 2
to the argument and then add 1
to the intermediate result...
44: {-@ plus3'' :: x:Int -> {v:Int | v = x + 3} @-} 45: plus3'' :: Int -> Int 46: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + 3))}plus3'' = (x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}plus {VV : (GHC.Types.Int) | (VV == (1 : int))}1) forall <q :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. (x:(GHC.Types.Int) -> {VV : (GHC.Types.Int)<p x> | true}) -> (y:(GHC.Types.Int) -> {VV : (GHC.Types.Int)<q y> | true}) -> x3:(GHC.Types.Int) -> exists [z:{VV : (GHC.Types.Int)<q x3> | true}].{VV : (GHC.Types.Int)<p z> | true}. (x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}plus {VV : (GHC.Types.Int) | (VV == (2 : int))}2)
but verification fails as we need a way to compose the refinements!
Problem What is a suitable description of the compose operator
_54: (.) :: (b -> c) -> (a -> b) -> (a -> c)
that lets us relate a
and c
via b
?
We can analyze the composition operator
With a very descriptive abstract refinement type!
69: 70: {-@ cc :: forall < p :: b -> c -> Prop 71: , q :: a -> b -> Prop>. 72: f:(x:b -> c<p x>) 73: -> g:(x:a -> b<q x>) 74: -> y:a 75: -> exists[z:b<q y>].c<p z> 76: @-} 77: 78: cc :: (b -> c) -> (a -> b) -> a -> c 79: forall a b c <p :: a-> b-> Bool, q :: c-> a-> Bool>. (x:a -> {VV : b<p x> | true}) -> (x:c -> {VV : a<q x> | true}) -> y:c -> exists [z:{VV : a<q y> | true}].{VV : b<p z> | true}cc x:a -> {VV : b | ((papp2 p VV x))}f x:a -> {VV : b | ((papp2 q VV x))}g ax = x:a -> {VV : b | ((papp2 p VV x))}f (x:a -> {VV : b | ((papp2 q VV x))}g {VV : a | (VV == x)}x)
We can verify the desired plus3
function:
88: {-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-} 89: plus3 :: Int -> Int 90: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + 3))}plus3 = (x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (1 : int))}1) forall <q :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. (x:(GHC.Types.Int) -> {VV : (GHC.Types.Int)<p x> | true}) -> (x:(GHC.Types.Int) -> {VV : (GHC.Types.Int)<q x> | true}) -> y:(GHC.Types.Int) -> exists [z:{VV : (GHC.Types.Int)<q y> | true}].{VV : (GHC.Types.Int)<p z> | true}`cc` (x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (2 : int))}2)
LiquidHaskell verifies the above, by instantiating
p
with v = x + 1
q
with v = x + 2
which lets it infer that the output of plus3
has type:
exists [z:{v=y+2}]. {v = z + 1}
which is a subtype of {v:Int | v = 3}