content: ---
  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**.
  
  <!-- more -->
  
  <div class="hidden">
  \begin{code}
  module BoundedRefinementTypes where
  import Prelude hiding ((.), maximum)
  import Language.Haskell.Liquid.Prelude
  
  incr  :: Int -> Int
  incr2 :: Int -> Int
  incr3 :: Int -> Int
  
  compose1 :: (Int -> Int) -> (Int -> Int) -> Int -> Int
  compose1 f g x = f (g x)
  incr2'     :: Int -> Int
  compose2 :: (b -> c) -> (a -> b) -> a -> c
  \end{code}
  </div>
  
  Reusable Specifications
  -----------------------
  
  Let us suppose, for just a moment, that we live in a dystopian future
  where parametric polymorphism and typeclasses have been eliminated
  from Haskell. Now, consider the function that returns the largest
  element of a list:
  
  \begin{code}
  maximum         :: [Int] -> Int
  maximum [x]    = x
  maximum (x:xs) = max x (maximum xs)
    where
      max a b    = if a < b then b else a
  \end{code}
  
  Now, suppose we have refinements:
  
  \begin{code}
  {-@ type Pos  = {v:Int | 0 < v} @-}
  {-@ type Neg  = {v:Int | 0 > v} @-}
  \end{code}
  
  **Here's the problem:** how can *specify* the behavior of `maximum`
  in a way that lets us verify that:
  
  \begin{code}
  {-@ posMax :: [Int] -> Pos @-}
  posMax xs = maximum [x | x <- xs, x > 0]
  
  {-@ negMax :: [Int] -> Neg @-}
  negMax xs = maximum [x | x <- xs, x < 0]
  \end{code}
  
  In the first case, the output of `maximum` must be
  a `Pos` because *every* input was a `Pos`. Thus, we
  might try to type:
  
  \begin{spec}
  maximum :: [Pos] -> Pos
  \end{spec}
  
  But this specification will not let us verify `negMax`.
  Thus, we have a problem: how can we write a precise
  specification for `maximum` that we can *reuse* at
  different call-sites. Further, how can we do so
  enumerating *a priori* the possible contexts (e.g.
  `Pos` and `Neg` lists) in which the function may
  be used?
  
  Abstracting Refinements
  -----------------------
  
  The first idea is one we've [seen before][AbstractRefinements].
  Notice that `maximum` returns _one of_ the elements in its input
  list. Thus, if *every* element of the list satisfies some
  refinement `p` then the output value is also guaranteed to
  satisfy `p`. We formalize this notion by *abstracting refinements*
  over type specifications. That is, we can type `maximum` as:
  
  \begin{code}
  {-@ maximum :: forall <p:: Int -> Prop>. [Int<p>] -> Int<p> @-}
  \end{code}
  
  Informally, `Int<p>` 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 analogous 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 <p :: b -> c -> Prop,
                            q :: a -> b -> Prop,
                            r :: a -> c -> Prop>.
                     (y:b -> c<p y>)
                  -> (x:a -> b<q x>)
                  -> x:a -> c<r x>                   @-}
  \end{code}
  
  With this type for `compose2` liquidHaskell will prove that composing `incr` by itself
  gives a function that increased its argument by `2`:
  
  \begin{code}
  {-@ incr2'' :: x:Int -> {v:Int | v = x + 2} @-}
  incr2''      = compose2 incr incr
  \end{code}
  
  To do so, liquidHaskell will employ the Abstract Refinement Types inference and guess
  the appropriate instantiations for `p`, `q`, and `r`.
  That is, liquidHaskell will infer that `p` and `q` relate two consecutive numbers
  `p, q := \x v -> v = x + 1`
  while `r` relates two numbers with distance `2`:
  `r := \x v -> v = x + 2`.
  Thus, at this specific call site the abstract type of `compose2` will be instantiated to
  the concrete type we gave to `compose1`.
  And, verification of `incr2''` will succeed.
  
  
  What is the catch now?
  In this second attempt we abstracted the type of `compose2` too much!
  In fact, LiquidHaskell cannot prove that the body of `compose2` satisfies its type, just because it does not.
  
  \begin{code}
  compose2 f g x = let z = g x in f z
  \end{code}
  
  By the precondition of `compose2` we know the result refinements of the functional arguments `f` and `g`.
  From the type of `g` we know that `z` satisfies `q` on `x`, i.e. `q x z` holds.
  Similarly, from the type of `f` we know that `f z` satisfies `q` on `x`, i.e. `q x z` holds.
  
  With these, liquidHaskell needs to prove that the result `f z` satisfies `r` on `x`, i.e., `r x z` holds.
  The required property `r x z` is not satisfied for _arbitrary_ abstract refinements `p`, `q` and `r`, but only for ones that satisfy a _chain property_ that states that for all `x`, `y` and `z`, if `q x y` and `p y z` holds, then `r x z` holds:
  
  <br>
  
  `\ 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 <p :: b -> c -> Prop,
                     q :: a -> b -> Prop,
                     r :: a -> c -> Prop>.
             (Chain b c a p q r)
          => (y:b -> c<p y>)
          -> (z:a -> b<q z>)
          ->  x:a -> c<r x>
  @-}
  \end{code}
  
  This type of `compose` is both sound and general enough,
  as now we can easily prove that composing `incr` with `incr2`
  results in a function that increases its argument by `3`.
  
  \begin{code}
  {-@ incr2''' :: x:Int -> {v:Int | v = x + 2} @-}
  incr2'''      = compose incr incr
  
  {-@ incr3'' :: x:Int -> {v:Int | v = x + 3} @-}
  incr3''      = compose incr2'' incr
  \end{code}
  
  
  Conclusion
  ----------
  We saw how bounds in refinement types allow us to specify a
  precise and general type for function composition.
  Bounds in refinement types are (haskell typeclases-like) constraints
  that constraint the abstract refinement variables to specify certain properties.
  
  We note that liquidHaskell desugars bounds to unbounded refinement types,
  thus verification is still performed decidably using the power of the SMT solvers.
  
  Moreover, function composition is not the exclusive user of
  Bounded Refinement Types.
  On the contrary, we used Bounded Refinement Types
  to verify a variety of code, from list-filtering to relational databases.
  
  Read more about bounds in our [ICFP'15 paper][icfp15],
  and stay tuned!
  
  <div class="hidden">
  \begin{code}
  \end{code}
  </div>
  
  
  [icfp15]: http://goto.ucsd.edu/~nvazou/icfp15/main.pdf
  [AbstractRefinements]: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/06/03/abstracting-over-refinements.lhs
  [queue-wiki]: http://en.wikipedia.org/wiki/Queue_%28abstract_data_type%29
  