Function Composition

```7: module Composition where
```

A Plus Function

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.

A Composed Variant

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` ?

Composing Refinements, Abstractly

• 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)
```

Using Composition

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}`