1 {-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-}
2 module LambdaCalculusInterpreter
4 import Prelude hiding ( id, (.) )
7 -- A two-stage (untyped) Lambda Calculus interpreter, from Hughes'
8 -- __Generalizing Monads to Arrows__.
12 -- Note how we have to use environment classifiers to tie Env, Val,
13 -- and Exp together (I miss Coq's [Section] command!!), yet the result
14 -- of "eval" is polymorphic in this classifier -- so long as the "Env"
15 -- and "Val" share it.
25 type Env c = [(Id,Val c)]
26 data Val c = Num Int | Fun <[Val c -> Val c]>@c
30 -- This won't work until I implement proper support for inductive
31 -- types in the guest language
35 eval :: Exp -> forall c. <[ Env c -> Val c ]>@c
37 eval (If e1 e2 e3) = <[ \env -> if ~~(eval e1)
41 eval (Add e1 e2) = <[ \env -> let (Num v1) = ~~(eval e1) env
42 in let (Num v2) = ~~(eval e2) env
45 eval (Lam x e) = <[ \env -> Fun (\v -> ~~(eval e) ((x,v):env)) ]>
47 eval (App e1 e2) = <[ \env -> case ~~(eval e1) env of
48 Fun f -> f ~~(eval e2) env ]>