total-eval.hs

0README.md

Total (non-error-throwing) lambda-calculus evaluators.

total-eval.hs

-- https://scm.iis.sinica.edu.tw/home/2008/typed-lambda-calculus-interprete/
-- and http://okmij.org/ftp/tagless-final/course/lecture.pdf which mentions this trick
--
-- this approach is inspectable; you can print the AST and manipulate it; count variable references, etc.

{-# LANGUAGE GADTs #-}

data Exp env t where
  C :: a -> Exp env a
  V :: Var env t -> Exp env t
  L :: Exp (a,env) b -> Exp env (a-> b)
  A :: Exp env (a-> b) -> Exp env a -> Exp env b

data Var env t where
  VZ :: Var (t, env) t
  VS :: Var env t -> Var (a, env) t

eval :: env -> Exp env t -> t
eval env (V v) = lookp v env
eval _   (C c) = c
eval env (L e) = \x -> eval (x, env) e
eval env (A e1 e2) = (eval env e1) (eval env e2)

lookp :: Var env t -> env -> t
lookp VZ (x,_)        = x
lookp (VS v) (_, env) = lookp v env

{-

Example: 

> eval () (A (L (V VZ)) (C 'a'))
'a'

-- const
> eval () (A (A (L (L (V (VS VZ)))) (C 'a')) (C 123))
'a'

-}

z-alt-total-but-not-inspectable.hs

-- this HOAS approach is total but not inspectable, so is of limited utility

-- λ> eval (A (L (\(C i) -> C (i * 2))) (C 2))
-- 4

{-# LANGUAGE GADTs #-}

data E a where
  C :: a -> E a
  L :: (E a -> E b) -> E (a -> b)
  A :: E (a -> b) -> E a -> E b

eval :: E a -> a
eval (L f) = \x -> eval (f (C x))
eval (A e1 e2) = (eval e1) (eval e2)
eval (C v) = v

-- see also https://gist.github.com/chrisdone/24e47c2952e4ad78c246