Case Study: Associative Maps & Evaluation


We've all been bitten by these!


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













Case Study: Associative Maps & Evaluation


Next, lets see how to use:


  • Sets to create safe associative maps

  • Measures to create well-scoped evaluators













Associative Maps













A Simple Associative Map


Lets start with the type definition:


data Map k v = Emp
             | Bind k v (Map k v)
               deriving (Eq, Ord, Show)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Tracking the Keys in a Map


We will banish unpleasant exceptions of the form:

*** Exception: key is not in the map ***


By tracking the set of defined keys in the API

keys   :: Map k v -> Set k

empty :: {m:Map k v | Set_emp (keys m)}

insert :: k:k -> v -> m:Map k v -> {m': Map k v | keys m' = add k m}

lookup :: k:k -> {m: Map | has k m} -> v













Specifying the Set of keys


Via a measure similar to elems of a List:


{-@ measure keys @-}
keys :: (Ord k) => Map k v -> S.Set k
keys Emp          = S.empty
keys (Bind k _ m) = add k m
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













The Empty Map

The empty map has no keys

{-@ empty :: {m:Map k v | Set_emp (keys m)} @-}
empty :: Map k v
empty = Emp
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Inserting a New Key-Value Binding


Adds the key to those of the old Map


{-@ insert :: k:_ -> _ -> m:_ -> {v: _ | keys v = add k m } @-}
insert :: k -> v -> Map k v -> Map k v
insert k v m = Bind k v m
{-@ inline add @-}
add :: (Ord k) => k -> Map k v -> S.Set k
add k kvs = S.singleton k `S.union` keys kvs
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Exercise: Looking Up a Key's Value


Q: Urgh! How can we prevent the impossible from happening?

{-@ lookup :: (Eq k) => k:k -> {m:Map k v | has k m} -> v @-}
lookup k' (Bind k v m)
  | k' == k   = v
  | otherwise = lookup k' m
lookup _  Emp = impossible "lookup"
{-@ inline has @-}
has :: (Ord k) => k -> Map k v -> Bool
has k m = True -- EXERCISE
-- HINT
--   keys     :: Map k v -> Set k
--   S.member :: k -> S.Set k -> Bool
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Key Not Found Begone!


Errors caught at compile time!


test      = [ lookup hs langs   -- Ok
            , lookup py langs   -- Err
            ]
  where
    langs = Bind hs "lazy"  $
            Bind js "eager" $
            Emp
    hs    = "haskell"
    js    = "javascript"
    py    = "python"
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Well-Scoped Evaluators













Expressions


Lets define a small language of Expr


data Var  = V String deriving (Eq, Ord, Show)
data Expr = Val  Int
          | Var  Var
          | Plus Expr Expr
          | Let  Var  Expr Expr
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Values


We can define values as a refinement of Expr


{-@ type Val = {v:Expr | isVal v} @-}
{-@ measure isVal @-}
isVal :: Expr -> Bool
isVal (Val _) = True
isVal _       = False
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Exercise: Operating on Values


Q: What's a suitable signature for plus?


plus (Val i) (Val j) = Val (i+j)
plus _         _     = impossible "plus"
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Environments


An Environment maps Variables to Values


{-@ type Env = Map Var Val @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Evaluate Using Environments


We can now eval an Expr as:


{-@ eval :: Env -> Expr -> Val @-}
eval _ i@(Val _)     = i
eval g (Var x)       = lookup x g
eval g (Plus e1 e2)  = plus (eval g e1) (eval g e2)
eval g (Let x e1 e2) = eval gx e2
  where
    gx               = insert x v1 g
    v1               = eval g e1
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Yikes! lookup is rejected!


How to ensure that Var is in Env?













Free Variables


eval looks-up Env for values of free variables


{-@ measure free @-}
free               :: Expr -> S.Set Var
free (Val _)       = S.empty
free (Var x)       = S.singleton x
free (Plus e1 e2)  = xs1 `S.union`  xs2
  where
    xs1            = free e1
    xs2            = free e2
free (Let x e1 e2) = xs1 `S.union` (xs2 `S.difference` xs)
  where
    xs1            = free e1
    xs2            = free e2
    xs             = S.singleton x
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Free Variables


For example in let x = 10 in x + y

  • y occurs free,
  • x occurs bound.


ghci> let e1 = Let (V "x") (Val 10)
                 (Plus (Var (V "x")) (Var (V "y")))

ghci> free e1
      fromList [V "y"]













Well-scoped Expressions


e is well-scoped in an env G if free variables of e are defined in G:


{-@ type ScopedExpr G = {e: Expr | wellScoped G e} @-}
{-@ inline wellScoped @-}
wellScoped :: Env -> Expr -> Bool
wellScoped g e = free e `S.isSubsetOf` keys g
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Exercise: Well-Scoped eval


Q: Can you go back and fix the type of eval so it is safe?













Exercise: Top-level Evaluation


A closed Expr can be evaluated in an empty environment.


{-@ type ClosedExpr = {e: Expr | closed e} @-}
{-@ topEval :: ClosedExpr -> Val @-}
topEval =  eval Emp
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: Fix the definition of closed so topEval is safe?


{-@ inline closed @-}
closed :: Expr -> Bool
closed e = True -- EXERCISE
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Exercise: Checked Top-level Evaluation


safeEval should work with any Expr and Env


Q: What is the right check ok such that safeEval verifies?


{-@ safeEval :: Env -> Expr -> Maybe Val @-}
safeEval g e
  | ok        = Just $ eval g e
  | otherwise = Nothing
  where
    ok        = True -- EXERCISE
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Continue


Next: Case Studies