examples/LambdaCalculusInterpreter.hs

   1 {-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-}
   2 module LambdaCalculusInterpreter
   3 where
   4 import Prelude hiding ( id, (.) )
   5
   6 --
   7 -- A two-stage (untyped) Lambda Calculus interpreter, from Hughes'
   8 -- __Generalizing Monads to Arrows__.
   9 --
  10
  11 --
  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.
  16 --
  17
  18 type Id    = String
  19 data Exp   = Var Id
  20            | Add Exp Exp
  21            | If  Exp Exp Exp
  22            | App Exp Exp
  23            | Lam Id  Exp
  24
  25 type Env c = [(Id,Val c)]
  26 data Val c = Num Int | Fun <[Val c -> Val c]>@c
  27
  28
  29 --
  30 -- This won't work until I implement proper support for inductive
  31 -- types in the guest language
  32 --
  33
  34 {-
  35 eval :: Exp -> forall c. <[ Env c -> Val c ]>@c
  36
  37 eval (If  e1 e2 e3) = <[ \env -> if   ~~(eval e1)
  38                                  then ~~(eval e2)
  39                                  else ~~(eval e3) ]>
  40
  41 eval (Add e1 e2)    = <[ \env -> let    (Num v1) = ~~(eval e1) env
  42                                  in let (Num v2) = ~~(eval e2) env
  43                                  in     (Num (v1+v2))         ]>
  44
  45 eval (Lam x e)      = <[ \env -> Fun (\v -> ~~(eval e) ((x,v):env)) ]>
  46
  47 eval (App e1 e2)    = <[ \env -> case ~~(eval e1) env of
  48                                    Fun f -> f ~~(eval e2) env ]>
  49 -}