# 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")]

"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

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

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]