Case Study: Associative Maps & Evaluation
















Associative Maps


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













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)













Lets Banish Missing Key Exceptions!


1. Refine the Type with defined keys

keys   :: Map k v -> Set k
type MapK k v Ks = {m:Map k v | keys m = Ks}

2. Refine the API to track keys

empty  :: MapK k v emp
insert :: k:k -> v -> m:Map k v -> MapK k v {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













The Empty Map


The empty map has no keys


{-@ empty :: {m:Map k v | noKeys m} @-} empty :: Map k v empty = Emp {-@ inline noKeys @-} noKeys :: (Ord k) => Map k v -> Bool noKeys m = keys m == S.empty













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.union (S.singleton k) (keys kvs)













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 fix using, -- keys :: Map k v -> Set k -- S.member :: k -> S.Set k -> Bool













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"











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













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













Exercise: Operating on Values


Q: What's a suitable signature for plus?


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













Environments


An Environment maps Variables to Values


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













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


Yikes! lookup is rejected! How to ensure that x::Var is in g::Env?













Free vs Bound Variables


For example in let x = 10 in x + y

  • y occurs free, i.e. defined outside,
  • x occurs bound, i.e. defined inside (as 10).


eval looks-up Env for values of free variables













Free Variables


Specify free variables as a measure

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













Free Variables: Example


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

ghci> free e1
      S.Set (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 = S.isSubsetOf (free e) (keys g)













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

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

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













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













Wrap Up: Associative Maps & Evaluation



  1. Missing key errors are everywhere (and annoying!)

  2. Use sets to refine associative map API

  3. Use measures to create well-scoped evaluators













Continue


Next: Case Studies


[Continue]