--- layout: post title: "Bounded Refinement Types" date: 2015-06-13 comments: true external-url: author: Niki Vazou published: true categories: bounded-refinements, abstract-refinements, function-composition demo: BoundedRefinementTypes.hs --- While refinement types let SMT solvers do a lot of the "boring" analysis, they are limited to decidable (first order) logics which can prevent us from writing *modular* and *reusable* specifications for *higher-order* functions. Next, lets see why modularity is important, and how we can recover it using a new technique called **Bounded Refinements**.
] -> Int
@-} \end{code} Informally, `Int
` stands for `{v:Int | p v}`, that is, `Int`s that satisfy the property `p`. The signature states that for any property `p` (of `Int`s), if the input is a list of elements satisfying `p` then the output is an `Int` satisfying `p`. We can coax SMT solvers into proving the above type by encoding `p v` as an [uninterpreted function](https://en.wikipedia.org/wiki/Uninterpreted_function) in the refinement logic. Thus, refinement abstraction is analagous to type abstraction: it lets us parameterize signatures over *all* refinements (analogously, types) that may be _passed in_ at the call-site. Capturing Dependencies between Relations ---------------------------------------- Unfortunately, in the dependent setting, this is not enough. Consider `incr` which bumps up its input by 1: \begin{code} {-@ incr :: x:Int -> {v:Int | v = x + 1} @-} incr x = x + 1 \end{code} We can use `incr` to write and check: \begin{code} {-@ incr2 :: x:Int -> {v:Int | v = x + 2} @-} incr2 x = let y = incr x z = incr y in z \end{code} LH uses the specification of `incr` to infer that + `y :: {v:Int | v = x + 1}` + `z :: {v:Int | v = y + 1}` and hence, that the result `z` equals `x + 2`. Now, you're probably wondering to yourself: isn't this what _function composition_ is for? Indeed! Lets define: \begin{code} {-@ compose' :: (b -> c) -> (a -> b) -> a -> c @-} compose' f g x = f (g x) \end{code} Now, we might try: \begin{code} {-@ incr2' :: x:Int -> {v:Int | v = x + 2} @-} incr2' = compose' incr incr \end{code} **Problem 1: Cannot Relate Abstracted Types** LH _rejects_ the above. This might seem counterintuitive but in fact, its the right thing to do given the specification of `compose'` -- at this call-site, each of `a`, `b` and `c` are instantiated with `Int` as we have no way of *relating* the invariants associated with those types, e.g. that `b` is one greater than `a` and `c` is one greater than `b`. **Problem 2: Cannot Reuse Concrete Types** At the other extreme, we might try to give compose a concrete signature: \begin{code} {-@ compose'' :: (y:Int -> {z:Int | z = y + 1}) -> (x:Int -> {z:Int | z = x + 1}) -> x:Int -> {z:Int | z = x + 2} @-} compose'' f g x = f (g x) \end{code} This time, LH does verify \begin{code} {-@ incr2'' :: x:Int -> {v:Int | v = x + 2} @-} incr2'' = compose'' incr incr \end{code} but this is a pyrhhic victory as we can only `compose` the toy `incr` function (with itself!) and any attempt to use it elsewhere will throw a type error. Goal: Relate Refinements But Keep them Abstract ----------------------------------------------- The above toy example illustrates the _real_ problem: how can we **relate** the invariants of the type parameters for `compose` while simultaneously keeping them **abstract** ? **Can Abstract Refinements Help?** HEREHEREHERE Onto abstracting the type of compose we follow the route of [Abstract Refinements][AbstractRefinements]. We make a second attempt to type function composition and give `compose2` a type that states that forall abstract refinements `p`, `q` and `r` if (1) the first functional argument `f` returns a value that satisfies a relation `p` with respect to its argument `y`, and (2) the second functional argument `g` returns a value that satisfies a relation `q` with respect to its argument `x`, then the result function returns a value that satisfies a relation `r` with respect to its argument `x`: \begin{code} {-@ compose''' :: forall
c -> Prop, q :: a -> b -> Prop, r :: a -> c -> Prop>. (y:b -> c
)
-> (x:a -> b c -> Prop,
q :: a -> b -> Prop,
r :: a -> c -> Prop>.
(Chain b c a p q r)
=> (y:b -> c )
-> (z:a -> b)
-> x:a -> c
`\ x y z -> q x y ==> p y z ==> r x z`
Bound Abstract Refinements by the Chain Property
------------------------------------------------
We made two attempts to type `compose`.
The first one "failed" as our type was unrealistically specific.
The second failed as it was unsoundly general.
In our third and final attempt
we give `compose` a type that is abstracted over three abstract refinements `p`, `q` and `r`.
But, this time the three refinements are not arbitrary:
they are bounded to satisfy the chain property.
We encode the chain property as a boolean Haskell function:
\begin{code}
chain :: (b -> c -> Bool) -> (a -> b -> Bool)
-> (a -> c -> Bool) -> a -> b -> c -> Bool
chain p q r = \ x y z -> q x y ==> p y z ==> r x z
\end{code}
Then we use the new liquidHaskell keyword `bound` to lift the
`chain` function into the a logical bound that
can be used to constrain abstract refinements
\begin{code}
{-@ bound chain @-}
\end{code}
The above bound annotation defines the bound `Chain` that is used as a
constraint that relates the abstract refinements `p`, `q` and `r`
in the type signature of `compose`
\begin{code}
{-@
compose :: forall )
-> x:a -> c