Well Scoped Evaluator

Case Study: Associative Maps & Evaluation

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

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

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

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

The Empty Map

The empty map has no keys

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

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

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

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 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

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

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

Continue

Next: Case Studies