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

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)













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



















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