content: ---
  layout: post
  title: "Putting Things In Order"
  date: 2013-07-29 16:12
  comments: true
  external-url:
  categories: abstract-refinements
  author: Niki Vazou and Ranjit Jhala
  published: true 
  demo: Order.hs
  ---
  
  Hello again! Since we last met, much has happened that
  we're rather excited about, and which we promise to get
  to in the fullness of time.
  
  Today, however, lets continue with our exploration of
  abstract refinements. We'll see that this rather innocent 
  looking mechanism packs quite a punch, by showing how 
  it can encode various **ordering** properties of 
  recursive data structures.
  
  <!-- more -->
  
  \begin{code}
  module PuttingThingsInOrder where
  
  import Prelude hiding (break)
  
  -- Haskell Type Definitions
  plusOnes                         :: [(Int, Int)]
  insertSort, mergeSort, quickSort :: (Ord a) => [a] -> [a]
  \end{code}
  
  Abstract Refinements
  --------------------
  
  \begin{code} Recall that *abstract refinements* are a mechanism that let us write and check types of the form
  maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p>
  \end{code}
  
  which states that the output of `maxInt` preserves 
  *whatever* invariants held for its two inputs as 
  long as both those inputs *also* satisfied those 
  invariants. 
  
  First, lets see how we can (and why we may want to) 
  abstractly refine data types. 
  
  Polymorphic Association Lists
  -----------------------------
  
  Suppose, we require a type for association lists. 
  Lets define one that is polymorphic over keys `k` 
  and values `v` 
  
  \begin{code}
  data AssocP k v = KVP [(k, v)]
  \end{code}
  
  Now, in a program, you might have multiple association
  lists, whose keys satisfy different properties. 
  For example, we might have a table for mapping digits 
  to the corresponding English string
  
  \begin{code}
  digitsP :: AssocP Int String
  digitsP = KVP [ (1, "one")
                , (2, "two")
                , (3, "three") ]
  \end{code}
  
  We could have a separate table for *sparsely* storing 
  the contents of an array of size `1000`.
  
  \begin{code}
  sparseVecP :: AssocP Int Double
  sparseVecP = KVP [ (12 ,  34.1 )
                   , (92 , 902.83)
                   , (451,   2.95)
                   , (877,   3.1 )]
  \end{code}
  
  The **keys** used in the two tables have rather 
  different properties, which we may want to track 
  at compile time.
  
  - In `digitsP` the keys are between `0` and `9` 
  - In `sparseVecP` the keys are between `0` and `999`. 
  
  Well, since we had the foresight to parameterize 
  the key type in `AssocP`, we can express the above 
  properties by appropriately **instantiating** the type
  of `k` with refined versions
  
  \begin{code}
  {-@ digitsP :: AssocP {v:Int | (Btwn 0 v 9)} String @-}
  \end{code}
  
  and 
  
  \begin{code}
  {-@ sparseVecP :: AssocP {v:Int | (Btwn 0 v 1000)} Double @-}
  \end{code}
  
  where `Btwn` is just an alias 
  
  \begin{code}
  {-@ predicate Btwn Lo V Hi = (Lo <= V && V <= Hi) @-}
  \end{code}
  
  Monomorphic Association Lists
  -----------------------------
  
  Now, suppose that for one reason or another, we want to 
  specialize our association list so that the keys are of 
  type `Int`. 
  
  \begin{code}
  data Assoc v = KV [(Int, v)]
  \end{code}
  
  (We'd probably also want to exploit the `Int`-ness 
  in the implementation but thats a tale for another day.)
  
  Now, we have our two tables
  
  \begin{code}
  digits    :: Assoc String
  digits    = KV [ (1, "one")
                 , (2, "two")
                 , (3, "three") ]
  
  sparseVec :: Assoc Double
  sparseVec = KV [ (12 ,  34.1 )
                 , (92 , 902.83)
                 , (451,   2.95)
                 , (877,   3.1 )]
  \end{code}
  
  but since we didn't make the key type generic, it seems 
  we have no way to distinguish between the invariants of 
  the two sets of keys. Bummer!
  
  Abstractly Refined Data
  -----------------------
  
  We *could* define *two separate* types of association 
  lists that capture different invariants, but frankly, 
  thats rather unfortunate, as we'd then have to 
  duplicate the code the manipulates the structures. 
  Of course, we'd like to have (type) systems help 
  keep an eye on different invariants, but we'd 
  *really* rather not have to duplicate code to 
  achieve that end. Thats the sort of thing that
  drives a person to JavaScript ;-).
  
  Fortunately, all is not lost. 
  
  If you were paying attention [last time][blog-absref] 
  then you'd realize that this is the perfect job for 
  an abstract refinement, this time applied to a `data` 
  definition:
  
  \begin{code}
  {-@ data Assoc v <p :: Int -> Prop> 
        = KV (z :: [(Int<p>, v)]) @-} 
  \end{code}
  
  The definition refines the type for `Assoc` to introduce
  an abstract refinement `p` which is, informally speaking,
  a property of `Int`. The definition states that each `Int`
  in the association list in fact satisfies `p` as, `Int<p>`
  is an abbreviation for `{v:Int| (p v)}`.
  
  Now, we can *have* our `Int` keys and *refine* them too!
  For example, we can write:
  
  \begin{code}
  {-@ digits :: Assoc (String) <{\v -> (Btwn 0 v 9)}> @-}
  \end{code}
  
  to track the invariant for the `digits` map, and write
  
  \begin{code}
  {-@ sparseVec :: Assoc Double <{\v -> (Btwn 0 v 1000)}> @-}
  \end{code}
  
  Thus, we can recover (some of) the benefits of abstracting 
  over the type of the key by instead parameterizing the type
  directly over the possible invariants. We will have much 
  [more to say][blog-absref-vec] on association lists 
  (or more generally, finite maps) and abstract refinements, 
  but lets move on for the moment.
  
  Dependent Tuples
  ----------------
  
  It is no accident that we have reused Haskell's function 
  type syntax to define abstract refinements (`p :: Int -> Prop`);
  interesting things start to happen if we use multiple parameters.
  
  Consider the function `break` from the Prelude. 
  
  \begin{code}
  break                   :: (a -> Bool) -> [a] -> ([a], [a])
  break _ xs@[]           =  (xs, xs)
  break p xs@(x:xs')
             | p x        =  ([], xs)
             | otherwise  =  let (ys, zs) = break p xs' 
                             in (x:ys,zs)
  \end{code}
  
  From the comments in [Data.List][data-list], `break p xs`: 
  "returns a tuple where the first element is longest prefix (possibly empty)
  `xs` of elements that do not satisfy `p` and second element is the 
  remainder of the list."
  
  We could formalize the notion of the *second-element-being-the-remainder* 
  using sizes. That is, we'd like to specify that the length of the second 
  element equals the length of `xs` minus the length of the first element.  
  That is, we need a way to allow the refinement of the second element to 
  *depend on* the value in the first refinement.
  Again, we could define a special kind of tuple-of-lists-type that 
  has the above property *baked in*, but thats just not how we roll.
  
  \begin{code} Instead, lets use abstract refinements to give us **dependent tuples**
  data (a,b)<p :: a -> b -> Prop> = (x:a, b<p x>) 
  \end{code}
  
  Here, the abstract refinement takes two parameters, 
  an `a` and a `b`. In the body of the tuple, the 
  first element is named `x` and we specify that 
  the second element satisfies the refinement `p x`, 
  i.e. a partial application of `p` with the first element. 
  In other words, the second element is a value of type
  `{v:b | (p x v)}`.
  
  As before, we can instantiate the `p` in *different* ways. 
  For example the whimsical
  
  \begin{code}
  {-@ plusOnes :: [(Int, Int)<{\x1 x2 -> x2 = x1 + 1}>] @-}
  plusOnes = [(0,1), (5,6), (999,1000)]
  \end{code}
  
  and returning to the *remainder* property for  `break` 
  
  \begin{code}
  {-@ break :: (a -> Bool) -> x:[a] 
            -> ([a], [a])<{\y z -> (Break x y z)}> @-}
  \end{code}
  
  using the predicate alias
  
  \begin{code}
  {-@ predicate Break X Y Z   = (len X) = (len Y) + (len Z) @-}
  \end{code}
  
  
  Abstractly Refined Lists
  ------------------------
  
  Right, we've been going on for a bit. Time to put things *in order*.
  
  To recap: we've already seen one way to abstractly refine lists: 
  to recover a *generic* means of refining a *monomorphic* list 
  (e.g. the list of `Int` keys.) However, in that case we were 
  talking about *individual* keys.
  Next, we build upon the dependent-tuples technique we just 
  saw to use abstract refinements to relate *different* 
  elements inside containers.
  
  In particular, we can use them to specify that *every pair* 
  of elements inside the list is related according to some 
  abstract relation `p`. By *instantiating* `p` appropriately,
  we will be able to recover various forms of (dis) order. 
  
  \begin{code} Consider the refined definition of good old Haskell lists:
  data [a] <p :: a -> a -> Prop> where
    | []  :: [a] <p>
    | (:) :: h:a -> [a<p h>]<p> -> [a]<p>
  \end{code}
  
  Whoa! Thats a bit of a mouthful. Lets break it down.
  
  * The type is parameterized with a refinement `p :: a -> a -> Prop` 
    Think of `p` as a *binary relation* over the `a` values comprising
    the list.
  
  * The empty list `[]` is a `[]<p>`. Clearly, the empty list has no
    elements whatsoever and so every pair is trivially, or rather, 
    vacuously related by `p`.
  
  * The cons constructor `(:)` takes a head `h` of type `a` and a tail
    of `a<p h>` values, each of which is *related to* `h` **and** which 
    (recursively) are pairwise related `[...]<p>` and returns a list where 
    *all* elements are pairwise related `[a]<p>`.
  
  Pairwise Related
  ----------------
  
  Note that we're being a bit sloppy when we say *pairwise* related.
  
  \begin{code} What we really mean is that if a list
  [x1,...,xn] :: [a]<p>
  \end{code}
  
  then for each `1 <= i < j <= n` we have `(p xi xj)`.
  
  \begin{code} To see why, consider the list
  [x1, x2, x3, ...] :: [a]<p>
  \end{code}
  
  \begin{code} This list unfolds into a head and tail 
  x1                :: a
  [x2, x3,...]      :: [a<p x1>]<p>
  \end{code}
  
  \begin{code} The above tail unfolds into
  x2                :: a<p x1>
  [x3, ...]         :: [a<p x1 && p x2>]<p>
  \end{code}
  
  \begin{code} And finally into 
  x3                :: a<p x1 && p x2>
  [...]             :: [a<p x1 && p x2 && p x3>]<p>
  \end{code}
  
  That is, each element `xj` satisfies the refinement 
  `(p xi xj)` for each `i < j`.
  
  Using Abstractly Refined Lists
  ------------------------------
  
  Urgh. *Math is hard!*  
  
  Lets see how we can *program* with these funnily refined lists.
  
  For starters, we can define a few helpful type aliases.
  
  \begin{code}
  {-@ type IncrList a = [a]<{\xi xj -> xi <= xj}> @-}      
  {-@ type DecrList a = [a]<{\xi xj -> xi >= xj}> @-}
  {-@ type UniqList a = [a]<{\xi xj -> xi /= xj}> @-}
  \end{code}
  
  As you might expect, an `IncrList` is a list of values in *increasing* order:
  
  \begin{code}
  {-@ whatGosUp :: IncrList Integer @-}
  whatGosUp = [1,2,3]
  \end{code}
  
  Similarly, a `DecrList` contains its values in *decreasing* order:
  
  \begin{code}
  {-@ mustGoDown :: DecrList Integer @-}
  mustGoDown = [3,2,1]
  \end{code}
  
  My personal favorite though, is a `UniqList` which has *no duplicates*:
  
  \begin{code}
  {-@ noDuplicates :: UniqList Integer @-}
  noDuplicates = [1,3,2]
  \end{code}
  
  Sorting Lists
  -------------
  
  Its all very well to *specify* lists with various kinds of invariants. 
  The question is, how easy is it to *establish* these invariants?
  
  Lets find out, by turning inevitably to that staple of all forms of
  formal verification: your usual textbook sorting procedures.
  
  **Insertion Sort**
  
  First up: insertion sort. Well, no surprises here:
  
  \begin{code}
  {-@ insertSort    :: (Ord a) => xs:[a] -> (IncrList a) @-}
  insertSort []     = []
  insertSort (x:xs) = insert x (insertSort xs) 
  \end{code}
  
  The hard work is done by `insert` which places an 
  element into the correct position of a sorted list
  
  \begin{code}
  insert y []     = [y]
  insert y (x:xs) 
    | y <= x      = y : x : xs 
    | otherwise   = x : insert y xs
  \end{code}
  
  LiquidHaskell infers that if you give `insert` an element 
  and a sorted list, it returns a sorted list.
  
  \begin{code}
  {-@ insert :: (Ord a) => a -> IncrList a -> IncrList a @-}
  \end{code}
  
  If you prefer the more Haskelly way of writing insertion sort, 
  i.e. with a `foldr`, that works too. Can you figure out why?
  
  \begin{code}
  {-@ insertSort' :: (Ord a) => [a] -> IncrList a @-}
  insertSort' xs  = foldr insert [] xs
  \end{code}
  
  **Merge Sort**
  
  Well, you know the song goes. First, we write a function 
  that **splits** the input into two parts:
  
  \begin{code}
  split          :: [a] -> ([a], [a])
  split (x:y:zs) = (x:xs, y:ys) 
    where 
      (xs, ys)   = split zs
  split xs       = (xs, [])
  \end{code}
  
  Then we need a function that **merges** two (sorted) lists
  
  \begin{code}
  merge xs []         = xs
  merge [] ys         = ys
  merge (x:xs) (y:ys) 
    | x <= y          = x : merge xs (y:ys)
    | otherwise       = y : merge (x:xs) ys
  \end{code}
  
  LiquidHaskell deduces that if both inputs are 
  ordered, then so is the output.
  
  \begin{code}
  {-@ merge :: (Ord a) => IncrList a 
                       -> IncrList a 
                       -> IncrList a 
    @-}
  \end{code}
  
  Finally, using the above functions we write `mergeSort`:
  
  \begin{code}
  {-@ mergeSort :: (Ord a) => [a] -> IncrList a @-}
  mergeSort []  = []
  mergeSort [x] = [x]
  mergeSort xs  = merge (mergeSort ys) (mergeSort zs) 
    where 
      (ys, zs)  = split xs
  \end{code}
  
  Lets see how LiquidHaskell proves the output type. 
  
  + The first two cases are trivial: for an empty 
    or singleton list, we can vacuously instantiate 
    the abstract refinement with *any* concrete 
    refinement.
  
  + For the last case, we can inductively assume 
   `mergeSort ys` and `mergeSort zs` are sorted 
    lists, after which the type inferred for 
    `merge` kicks in, allowing LiquidHaskell to conclude
    that the output is also sorted.
  
  **Quick Sort**
  
  The previous two were remarkable because they were, well, quite *unremarkable*. 
  Pretty much the standard textbook implementations work *as is*. 
  Unlike the [classical][omega-sort] [developments][hasochism] 
  using indexed types we don't have to define any auxiliary 
  types for increasing lists, or lists whose value is in a 
  particular range, or any specialized `cons` operators and 
  so on.
  
  With *quick sort* we need to do a tiny bit of work.
  
  
  \begin{code} We would like to define `quickSort` as
  {-@ quickSort'    :: (Ord a) => [a] -> IncrList a @-}
  quickSort' []     = []
  quickSort' (x:xs) = lts ++ (x : gts) 
    where 
      lts           = quickSort' [y | y <- xs, y < x]
      gts           = quickSort' [z | z <- xs, z >= x]
  \end{code}
  
  But, if you try it out, you'll see that LiquidHaskell 
  *does not approve*. What could possibly be the trouble?
  
  The problem lies with *append*. What type do we give `++`? 
  
  \begin{code} We might try something like
  (++) :: IncrList a -> IncrList a -> IncrList a
  \end{code}
  
  \begin{code} but of course, this is bogus, as 
  [1,2,4] ++ [3,5,6]
  \end{code}
  
  is decidedly not an `IncrList`!
  
  Instead, at this particular use of `++`, there is
  an extra nugget of information: there is a *pivot*
  element `x` such that every element in the first 
  argument is less than `x` and every element in 
  the second argument is greater than `x`. 
  
  There is no way we can give the usual append `++` 
  a type that reflects the above as there is no pivot 
  `x` to refer to. Thus, with a heavy heart, we must
  write a specialized pivot-append that uses this fact:
  
  \begin{code}
  pivApp piv []     ys  = piv : ys
  pivApp piv (x:xs) ys  = x   : pivApp piv xs ys
  \end{code}
  
  Now, LiquidHaskell infers that 
  
  \begin{code}
  {-@ pivApp :: piv:a 
             -> IncrList {v:a | v <  piv} 
             -> IncrList {v:a | v >= piv} 
             -> IncrList a 
    @-}
  \end{code}
  
  And we can use `pivApp` to define `quickSort' simply as:
  
  \begin{code}
  {-@ quickSort    :: (Ord a) => [a] -> IncrList a @-}
  quickSort []     = []
  quickSort (x:xs) = pivApp x lts gts 
    where 
      lts          = quickSort [y | y <- xs, y < x ]
      gts          = quickSort [z | z <- xs, z >= x]
  \end{code}
  
  Really Sorting Lists
  --------------------
  
  The convenient thing about our encoding is that the 
  underlying datatype is plain Haskell lists. 
  This yields two very concrete benefits. 
  First, as mentioned before, we can manipulate 
  sorted lists with the same functions we'd use 
  for regular lists.
  Second, by decoupling (or rather, parameterizing)
  the relation or property or invariant from the actual 
  data structure we can plug in different invariants, 
  sometimes in the *same* program.
  
  To see why this is useful, lets look at a *real-world* 
  sorting algorithm: the one used inside GHC's 
  `Data.List` [module][data-list].
  
  \begin{code}
  sort :: (Ord a) => [a] -> [a]
  sort = mergeAll . sequences
    where
      sequences (a:b:xs)
        | a `compare` b == GT = descending b [a]  xs
        | otherwise           = ascending  b (a:) xs
      sequences [x] = [[x]]
      sequences []  = [[]]
  
      descending a as (b:bs)
        | a `compare` b == GT = descending b (a:as) bs
      descending a as bs      = (a:as): sequences bs
  
      ascending a as (b:bs)
        | a `compare` b /= GT = ascending b (\ys -> as (a:ys)) bs
      ascending a as bs       = as [a]: sequences bs
  
      mergeAll [x] = x
      mergeAll xs  = mergeAll (mergePairs xs)
  
      mergePairs (a:b:xs) = merge a b: mergePairs xs
      mergePairs [x]      = [x]
      mergePairs []       = []
  \end{code}
  
  The interesting thing about the procedure is that it 
  generates some intermediate lists that are increasing 
  *and* others that are decreasing, and then somehow
  miraculously whips this whirlygig into a single 
  increasing list.
  
  Yet, to check this rather tricky algorithm with 
  LiquidHaskell we need merely write:
  
  \begin{code}
  {-@ sort :: (Ord a) => [a] -> IncrList a  @-}
  \end{code}
  
  
  
  [blog-absref]:     /blog/2013/06/3/abstracting-over-refinements.lhs/
  [blog-absref-vec]: http://goto.ucsd.edu/~rjhala/liquid/abstract_refinement_types.pdf
  [data-list]:        http://www.haskell.org/ghc/docs/latest/html/libraries/base/src/Data-List.html#sort
  [omega-sort]:      http://web.cecs.pdx.edu/~sheard/Code/InsertMergeSort.html
  [hasochism]:       https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf
  
  