content: 
  Case Study: Associative Maps
  ============================
  
  \begin{comment}
  \begin{code}
  {-@ LIQUID "--no-termination" @-}
  
  module Tutorial_10_Case_Study_Associative_Maps where
  
  import Data.Set hiding (elems)
  -- | Boilerplate
  
  {-@ die :: {v:_ | false} -> a @-}
  die x   = error x
  
  -- | Haskell Definitions
  
  data Map k v = Node { key   :: k
                      , value :: v
                      , left  :: Map k v
                      , right :: Map k v }
               | Tip
  
  lemma_notMem :: k -> Map k v -> Bool
  set    :: (Ord k) => k -> v -> Map k v -> Map k v
  get    :: (Ord k) => k -> Map k v -> v
  get'   :: (Ord k) => k -> Map k v -> v
  mem    :: (Ord k) => k -> Map k v -> Bool
  emp    :: Map k v
  elems  :: (Ord a) => [a] -> Set a
  fresh  :: [Int] -> Int
  
  -- | Set Interface
  {-@ predicate In X Xs      = Set_mem X Xs               @-}
  {-@ predicate Subset X Y   = Set_sub X Y                @-}
  {-@ predicate Empty  X     = Set_emp X                  @-}
  {-@ predicate Union X Y Z  = X = Set_cup Y Z            @-}
  {-@ predicate Union1 X Y Z = Union X (Set_sng Y) Z      @-}
  
  -- | Predicate Aliases
  {-@ predicate NoKeys M     = Empty (keys M)             @-}
  {-@ predicate HasKey K M   = In K (keys M)              @-}
  {-@ predicate AddKey K M N = Union1 (keys N) K (keys M) @-}
  
  -- {-@ ignore tests @-}
  -- {-@ ignore set   @-}
  -- {-@ ignore get   @-}
  -- {-@ ignore get'  @-}
  -- {-@ ignore mem   @-}
  
  \end{code}
  \end{comment}
  
  \begin{comment}
  \begin{figure}[h]
  \includegraphics[height=1.0in]{img/piponi-tweet.png}
  \caption{Wouldn't it be nice to know that a key was in a map?}
  \label{fig:piponi-tweet}
  \end{figure}
  \end{comment}
  
  Recall the following from the [introduction](#intro):
  
  ~~~~~{.ghci}
  ghci> :m +Data.Map
  ghci> let m = fromList [ ("haskell"   , "lazy")
                         , ("javascript", "eager")]
  
  ghci> m ! "haskell"
  "lazy"
  
  ghci> m ! "python"
  "*** Exception: key is not in the map
  ~~~~~
  
  \noindent
  The problem illustrated above is quite a pervasive one; associative
  maps pop up everywhere. Failed lookups are the equivalent of
  `NullPointerDereference` exceptions in languages like Haskell.
  It is rather difficult to use Haskell's type system to precisely
  characterize the behavior of associative map APIs as ultimately,
  this requires tracking the *dynamic set of keys* in the map.
  
  In this case study, we'll see how to combine two techniques,
  [measures](#setmeasure) and [refined data types](#refineddatatypes),
  to analyze programs that *implement* and *use* associative
  maps (e.g. `Data.Map` or `Data.HashMap`).
  
  Specifying Maps {#mapapi}
  -------------------------
  
  Lets start by defining a *refined API* for Associative Maps
  that tracks the set of keys stored in the map, in order to
  statically ensure the safety of lookups.
  
  \newthought{Types} First, we need a type for `Map`s. As usual,
  let's parameterize the type with `k` for the type of keys and
  `v` for the type of values:
  
  ~~~~~{.spec}
  data Map k v    -- Currently left abstract
  ~~~~~
  
  \newthought{Keys} To talk about the set of keys in a map,
  we will use a *measure*
  
  ~~~~~{.spec}
  measure keys :: Map k v -> Set k
  ~~~~~
  
  \noindent that associates each `Map` to the `Set` of its
  defined keys. Next, we use the above measure, and the usual
  `Set` operators to refine the types of the functions that
  *create*, *add* and *lookup* key-value bindings, in order
  to precisely track, within the type system, the `keys`
  that are dynamically defined within each `Map`. ^[Recall
  that `Empty`, `Union`, `In` and the other `Set` operators
  are described [here](#listelems).]
  
  \newthought{Empty} `Map`s have no keys in them. Hence, we type
  the empty `Map` as:
  
  ~~~~~{.spec}
  emp :: {m:Map k v | Empty (keys m)}
  ~~~~~
  
  \newthought{Add} The function `set` takes a key $k$ a
  value $v$ and a map `m` and returns the new map obtained
  by extending `m` with the binding ${k \mapsto v}$.
  Thus, the set of `keys` of the output `Map` includes
  those of the input plus the singleton $k$, that is:
  
  ~~~~~{.spec}
  set :: k:k -> v -> m:Map k v -> {n: Map k v| AddKey k m n}
  
  predicate AddKey K M N = keys N = Set_cup (Set_sng K) (keys M)
  ~~~~~
  
  \newthought{Query} Finally, queries will only succeed for
  keys that are defined a given `Map`. Thus, we define an alias:
  
  ~~~~~{.spec}
  predicate HasKey K M = In K (keys M)
  ~~~~~
  
  \noindent and use it to type `mem` which *checks* if
  a key is defined in the `Map` and `get` which actually
  returns the value associated with a given key.
  
  ~~~~~{.spec}
  -- | Check if key is defined
  mem :: k:k -> m:Map k v -> {v:Bool | v <=> HasKey k m}
  
  -- | Lookup key's value
  get :: k:k -> {m:Map k v | HasKey k m} -> v
  ~~~~~
  
  Using Maps: Well Scoped Expressions
  -----------------------------------
  
  Rather than jumping into the *implementation* of the above `Map` API,
  let's write a *client* that uses `Map`s to implement an interpreter for
  a tiny language. In particular, we will use maps as an *environment*
  containing the values of *bound variables*, and we will use the refined
  API to ensure that *lookups never fail*, and hence, that well-scoped
  programs always reduce to a value.
  
  \newthought{Expressions} Lets work with a simple language with
  integer constants, variables, binding and arithmetic operators:^[Feel
  free to embellish the language with fancier features like functions,
  tuples etc.]
  
  \begin{code}
  type Var  = String
  
  data Expr = Const Int
            | Var   Var
            | Plus  Expr Expr
            | Let   Var  Expr Expr
  \end{code}
  
  \newthought{Values} We can use refinements to formally
  describe *values* as a subset of `Expr` allowing us to
  reuse a bunch of code. To this end, we simply define a
  (`measure`) predicate characterizing values:
  
  \begin{code}
  {-@ measure val @-}
  val              :: Expr -> Bool
  val (Const _)    = True
  val (Var _)      = False
  val (Plus _ _)   = False
  val (Let _ _ _ ) = False
  \end{code}
  
  \noindent and then we can use the lifted `measure` to
  define an alias for `Val` denoting values:
  
  \begin{code}
  {-@ type Val = {v:Expr | val v} @-}
  \end{code}
  
  \noindent we can use the above to write simple *operators*
  on `Val`, for example:
  
  \begin{code}
  {-@ plus                 :: Val -> Val -> Val @-}
  plus (Const i) (Const j) = Const (i+j)
  plus _         _         = die "Bad call to plus"
  \end{code}
  
  \newthought{Environments} let us save values for the
  local" i.e. *let-bound* variables; when evaluating
  an expression `Var x` we simply look up the value of
  `x` in the environment. This is why `Map`s were
  invented! Lets define our environments as `Map`s from `Var`iables to `Val`ues:
  
  \begin{code}
  {-@ type Env = Map Var Val @-}
  \end{code}
  
  \noindent The above definition essentially specifies, inside the
  types, an *eager* evaluation strategy: LiquidHaskell will prevent
  us from sticking unevaluated `Expr`s inside the environments.
  
  \newthought{Evaluation} proceeds via a straightforward recursion
  over the structure of the expression. When we hit a `Var` we simply
  query its value from the environment. When we hit a `Let` we compute
  the bound expression and tuck its value into the environment before
  proceeding within.
  
  \begin{code}
  eval _ i@(Const _)   = i
  eval g (Var x)       = get x g
  eval g (Plus e1 e2)  = plus  (eval g e1) (eval g e2)
  eval g (Let x e1 e2) = eval g' e2
    where
      g'               = set x v1 g
      v1               = eval g e1
  \end{code}
  
  The above `eval` seems rather unsafe; whats the guarantee that
  `get x g` will succeed? For example, surely trying:
  
  ~~~~~{.ghci}
  ghci> eval emp (Var "x")
  ~~~~~
  
  \noindent will lead to some unpleasant crash. Shouldn't we *check*
  if the variables is present and if not, fail with some sort of
  `Variable Not Bound` error? We could, but we can do better: we can
  prove at compile time, that such errors will not occur.
  
  \newthought{Free Variables} are those whose values are *not* bound
  within an expression, that is, the set of variables that *appear* in
  the expression, but are not *bound* by a dominating `Let`. We can
  formalize this notion as a (lifted) function:
  
  \begin{code}
  {-@ measure free @-}
  free               :: Expr -> (Set Var)
  free (Const _)     = empty
  free (Var x)       = singleton x
  free (Plus e1 e2)  = xs1 `union`  xs2
    where
      xs1            = free e1
      xs2            = free e2
  free (Let x e1 e2) = xs1 `union` (xs2 `difference` xs)
    where
      xs1            = free e1
      xs2            = free e2
      xs             = singleton x
  \end{code}
  
  \newthought{An Expression is Closed} with respect to an environment
  `G` if all the *free* variables in the expression appear in `G`, i.e.
  the environment contains bindings for all the variables in the
  expression that are *not* bound within the expression. As we've seen
  repeatedly, often a whole pile of informal hand-waving, can be
  succinctly captured by a type definition that says the `free` variables
  in the `Expr` must be contained in the `keys` of the environment `G`:
  
  \begin{code}
  {-@ type ClosedExpr G = {v:Expr | Subset (free v) (keys G)} @-}
  \end{code}
  
  \newthought{Closed Evaluation} never goes wrong, i.e. we can
  ensure that `eval` will not crash with unbound variables, as
  long as it is invoked with suitable environments:
  
  \begin{code}
  {-@ eval :: g:Env -> ClosedExpr g -> Val @-}
  \end{code}
  
  \noindent We can be sure an `Expr` is well-scoped if it has *no*
  free variables.Lets use that to write a "top-level" evaluator:
  
  \begin{code}
  {-@ topEval :: {v:Expr | Empty (free v)} -> Val @-}
  topEval     = eval emp
  \end{code}
  
  <div class="hwex" id="Wellformedness Check"> Complete the definition
  of the below function which *checks* if an `Expr` is well formed
  before `eval`uating it:
  </div>
  
  \begin{code}
  {-@ evalAny   :: Env -> Expr -> Maybe Val @-}
  evalAny g e
    | ok        = Just $ eval g e
    | otherwise = Nothing
    where
      ok        = undefined
  \end{code}
  
  \noindent Proof is all well and good, in the end, you need a few
  sanity tests to kick the tires. So:
  
  \begin{code}
  tests   = [v1, v2]
    where
      v1  = topEval e1          -- Rejected by LH
      v2  = topEval e2          -- Accepted by LH
      e1  = (Var x) `Plus` c1
      e2  = Let x c10 e1
      x   = "x"
      c1  = Const 1
      c10 = Const 10
  \end{code}
  
  <div class="hwex" id="Closures">
  \doublestar Extend the language above to include functions.
  That is, extend `Expr` as below, (and `eval` and `free` respectively.)
  </div>
  
  ~~~~~{.spec}
  data Expr = ... | Fun Var Expr | App Expr Expr
  ~~~~~
  
  Just focus on ensuring the safety of variable lookups;
  ensuring full type-safety (i.e. every application is to
  a function) is rather more complicated and beyond the
  scope of what we've seen so far.
  
  
  Implementing Maps: Binary Search Trees {#lemmas}
  --------------------------------------
  
  We just saw how easy it is to *use* the Associative
  Map [API](#mapapi) to ensure the safety of lookups,
  even though the `Map` has a "dynamically" generated
  set of keys. Next, let's see how we can *implement*
  a `Map` library that respects the API using
  [Binary Search Trees](#binarysearchtree)
  
  \newthought{Data Type} First, let's provide an
  implementation of the hitherto abstract data
  type for `Map`. We shall use Binary Search Trees,
  wherein, at each `Node`, the `left` (resp. `right`)
  subtree has keys that are less than (resp. greater than)
  the root `key`.
  
  \begin{code}
  {-@ data Map k v = Node { key   :: k
                          , value :: v
                          , left  :: Map {v:k | v < key} v
                          , right :: Map {v:k | key < v} v }
                   | Tip
    @-}
  \end{code}
  
  [Recall](#binarysearchtree) that the above
  refined data definition yields strengthened data
  constructors that statically ensure that only legal,
  *binary-search ordered* trees are created in the program.
  
  \newthought{Defined Keys} Next, we must provide an
  implementation of the notion of the `keys` that are
  defined for a given `Map`.  This is achieved via the
  lifted measure function:
  
  \begin{code}
  {-@ measure keys @-}
  keys                :: (Ord k) => Map k v -> Set k
  keys Tip            = empty
  keys (Node k _ l r) = ks `union` kl `union` kr
    where
      kl              = keys l
      kr              = keys r
      ks              = singleton k
  
  \end{code}
  
  Armed with the basic type and measure definition, we
  can start to fill in the operations for `Maps`.
  
  <div class="hwex" id="Empty Maps">
  To make sure you are following, fill in the definition for an `emp`ty Map:
  </div>
  
  \begin{code}
  {-@ emp :: {m:Map k v | Empty (keys m)} @-}
  emp     = undefined
  \end{code}
  
  <div class="hwex" id="Insert"> To add a key `k'` to a `Map` we
  recursively traverse the `Map` zigging `left` or `right`
  depending on the result of comparisons with the keys along
  the path. Unfortunately, the version below has an
  (all too common!) bug, and hence, is *rejected*
  by LiquidHaskell. Find and fix the bug so that
  the function is verified.
  </div>
  
  \begin{code}
  {-@ set :: (Ord k) => k:k -> v -> m:Map k v
                     -> {n: Map k v | AddKey k m n} @-}
  set k' v' (Node k v l r)
    | k' == k   = Node k v' l r
    | k' <  k   = set k' v l
    | otherwise = set k' v r
  set k' v' Tip = Node k' v' Tip Tip
  \end{code}
  
  \newthought{Lookup} Next, let's write the `mem` function that returns
  the value associated with a key `k'`. To do so we just compare `k'`
  with the root key, if they are equal, we return the binding, and
  otherwise we go down the `left` (resp. `right`) subtree if sought for
  key is less (resp. greater) than the root `key`. Crucially, we want to
  check that lookup *never fails*, and hence, we implement the `Tip`
  (i.e. empty) case with `die` gets LiquidHaskell to prove that that
  case is indeed dead code, i.e. never happens at run-time.
  
  \begin{code}
  {-@ get' :: (Ord k) =>  k:k -> m:{Map k v| HasKey k m} -> v @-}
  get' k' m@(Node k v l r)
    | k' == k   = v
    | k' <  k   = get' k' l
    | otherwise = get' k' r
  get'  _ Tip   = die  "Lookup Never Fails"
  \end{code}
  
  \newthought{Unfortunately} the function above is *rejected*
  by LiquidHaskell. This is a puzzler (and a bummer!) because
  in fact it *is* correct. So what gives?
  Well, let's look at the error for the call `get' k' l`
  
  ~~~~~{.liquiderror}
   src/07-case-study-associative-maps.lhs:411:25: Error: Liquid Type Mismatch
     Inferred type
       VV : Map a b | VV == l
     not a subtype of Required type
       VV : Map a b | Set_mem k' (keys VV)
     In Context
       VV : Map a b | VV == l
       k  : a
       l  : Map a b
       k' : a
  ~~~~~
  
  \noindent LiquidHaskell is *unable* to deduce that the key `k'`
  definitely belongs in the `left` subtree `l`. Well, let's ask ourselves:
  *why* must `k'` belong in the left subtree? From the input, we know
  `HasKey k' m` i.e. that `k'` is *somewhere* in `m`.
  That is *one of* the following holds:
  
  1. `k' == k` or,
  2. `HasKey k' l` or,
  3. `HasKey k' r`.
  
  As the preceding guard `k' == k` fails, we (and LiquidHaskell)
  can rule out case (1). Now, what about the `Map` tells us that
  case (2) must hold, i.e. that case (3) cannot hold? The *BST invariant*,
  all keys in `r` exceed `k` which itself exceeds `k'`. That is,
  all nodes in `r` are *disequal* to `k'` and hence `k'` cannot
  be in `r`, ruling out case (3). Formally, we need the fact that:
  $$\forall\ \vkey,\ \vt. \vt :: {\vMap\ \reft{\vkey'}{k}{\vkey' \not = \vkey}\ v}
                          \ \Rightarrow\
                          \lnot (\vHasKey\ \vkey\ \vt)$$
  
  \newthought{Conversion Lemmas} Unfortunately, LiquidHaskell
  *cannot automatically* deduce facts like the above, as they
  relate refinements of a container's *type parameters*
  (here: $\vkey' \not = \vkey$, which refines the `Map`s first type
  parameter) with properties of the entire container
  (here: $\vHasKey\ \vkey\ \vt$).
  Fortunately, it is easy to *state*, *prove* and *use*
  facts like the above, via *lemmas* which are just functions. ^[Why
  does LiquidHaskell not automatically deduce this information? This
  is tricky to describe. Intuitively, because there is no way of
  automatically connecting the *traversal* corresponding to `keys`
  with the type variable `k`. I wish I had a better way to explain
  this rather subtle point; suggestions welcome!]
  
  \newthought{Defining Lemmas} To state a lemma, we need only
  convert it into a [type](curry-howard) by viewing universal
  quantifiers as function parameters, and implications as
  function types:
  
  \begin{code}
  {-@ lemma_notMem :: key:k
                   -> m:Map {k:k | k /= key} v
                   -> {v:Bool | not (HasKey key m)}
    @-}
  lemma_notMem _   Tip            = True
  lemma_notMem key (Node _ _ l r) = lemma_notMem key l &&
                                    lemma_notMem key r
  \end{code}
  
  \newthought{Proving Lemmas} Note how the signature for `lemma_notMem`
  corresponds exactly to the missing fact from above. The "output" type
  is a `Bool` refined with the proposition that we desire. We *prove*
  the lemma simply by *traversing* the tree which lets LiquidHaskell
  build up a proof for the output fact by inductively combining the
  proofs from the subtrees.
  
  \newthought{Using Lemmas} To use a lemma, we need to *instantiate*
  it to the particular keys and trees we care about, by "calling" the
  lemma function, and forcing its result to be in the *environment* used
  to typecheck the expression where we want to use the lemma. Say what?
  Here's how to use lemmas to verify `get`:
  
  \begin{code}
  {-@ get :: (Ord k) => k:k -> m:{Map k v | HasKey k m} -> v @-}
  get k' (Node k v l r)
    | k' == k   = v
    | k' <  k   = assert (lemma_notMem k' r) $
                    get k' l
    | otherwise = assert (lemma_notMem k' l) $
                    get k' r
  get _ Tip     = die "Lookup failed? Impossible."
  \end{code}
  
  By calling `lemma_notMem` we create a dummy `Bool` refined with
  the fact `not (HasKey k' r)` (resp. `not (HasKey k' l)`).
  We force the calls to `get k' l` (resp. `get k' r`) to be
  typechecked using the materialized refinement by wrapping
  the calls in `assert`:
  
  \begin{code}
  assert _ x = x
  \end{code}
  
  \newthought{Ghost Values} This technique of materializing auxiliary
  facts via *ghost values* is a well known idea in program
  verification. Usually, one has to take care to ensure that ghost
  computations do not interfere with the regular computations. If we had
  to actually *execute* `lemma_notMem` it would wreck the efficient
  logarithmic lookup time, assuming we kept the trees
  [balanced](#avltrees), as we would traverse the *entire* tree instead
  of just the short path to a node. ^[Which is what makes dynamic contract
  checking [inefficient](findler-contract) for such invariants.]
  
  \newthought{Laziness} comes to our rescue: as the ghost value is (trivially)
  not needed, it is never computed. In fact, it is straightforward to entirely
  *erase* the call in the compiled code, which lets us freely `assert` such
  `lemma`s to carry out proofs, without paying any runtime penalty. In an eager
  language we would have to do a bit of work to specifically mark the computation
  as a ghost or [irrelevant](proof-irrelevance) but in the lazy setting we get
  this for free.
  
  <div class="hwex" id="Membership Test"> Capisce? Fix the definition of `mem`
  so that it verifiably implements the given signature.
  </div>
  
  \begin{code}
  {-@ mem :: (Ord k) => k:k -> m:Map k v
                     -> {v:_ | v <=> HasKey k m} @-}
  mem k' (Node k _ l r)
    | k' == k   = True
    | k' <  k   = mem k' l
    | otherwise = mem k' r
  mem _ Tip     = False
  \end{code}
  
  <div class="hwex" id="Fresh">
  \doublestar To make sure you really understand this business of
  ghosts values and proofs, complete the implementation of the following function which
  returns a `fresh` integer that is *distinct* from all the values in its input list:
  </div>
  
  \begin{code}
  {-@ fresh :: xs:[Int] -> {v:Int | not (Elem v xs)} @-}
  fresh = undefined
  \end{code}
  
  \noindent To refresh your memory, here are the definitions for `Elem`
  we [saw earlier](#listelems)
  
  \begin{code}
  {-@ predicate Elem X Ys  = In X (elems Ys) @-}
  {-@ measure elems @-}
  elems []     = empty
  elems (x:xs) = (singleton x) `union` (elems xs)
  \end{code}
  
  Recap
  -----
  
  In this chapter we saw how to combine several of the techniques from previous chapters
  in a case study. We learned how to:
  
  1. *Define* an API for associative maps that used refinements to track the *set* of `keys`
     stored in a map, in order to prevent lookup failures, the `NullPointerDereference` errors
     of the functional world,
  
  2. *Use* the API to implement a small interpreter that is guaranteed to never fail with
     `UnboundVariable` errors, as long as the input expressions were closed,
  
  3. *Implement* the API using Binary Search Trees; in particular, using *ghost lemmas*
     to `assert` facts that LiquidHaskell is otherwise unable to deduce automatically.
  