Simple normalization by evaluation for the simply-typed lambda calculus

StlcNbE.hs

module StlcNbE where

data Term =
  Point
  | Lam Term
  | App Term Term
  | Pair Term Term
  | Proj1 Term
  | Proj2 Term
  | Var Int
  deriving Show
data Type =
  Unit
  | Primitive
  | Fun Type Type
  | Prod Type Type
  deriving Show
data Value =
  VPoint
  | VLam (Value -> Value)
  | VPair Value Value
  | Reflect Type Neutral
data Neutral =
  NVar Int
  | NApp Neutral Type Value
  | NProj1 Neutral
  | NProj2 Neutral

eval :: [Value] -> Term -> Value
eval c (Point) = VPoint
eval c (Lam x) = VLam (\a -> eval (a:c) x)
eval c (App f a) = vApp (eval c f) (eval c a)
eval c (Pair a b) = VPair (eval c a) (eval c b)
eval c (Proj1 p) = fst $ vProjs $ eval c p
eval c (Proj2 p) = snd $ vProjs $ eval c p
eval c (Var n) = c !! n

vApp :: Value -> Value -> Value
vApp (VLam f) a = f a
vApp (Reflect (Fun c d) f) a = Reflect d (NApp f c a)

vProjs :: Value -> (Value, Value)
vProjs (VPair a b) = (a, b)
vProjs (Reflect (Prod a b) p) =
  (Reflect a $ NProj1 p, Reflect b $ NProj2 p)

quote :: Int -> Type -> Value -> Term
quote n (Unit) _ = Point
quote n (Primitive) (Reflect Primitive e) = quoteNeutral n e
quote n (Fun c d) f = Lam $ quote (n+1) d $ vApp f (Reflect c $ NVar n)
quote n (Prod a b) p = Pair (quote n a $ fst p') (quote n b $ snd p')
  where p' = vProjs p

quoteNeutral :: Int -> Neutral -> Term
quoteNeutral n (NVar k) = Var $ n - (k + 1)
quoteNeutral n (NApp f t a) = App (quoteNeutral n f) (quote n t a)
quoteNeutral n (NProj1 e) = Proj1 $ quoteNeutral n e
quoteNeutral n (NProj2 e) = Proj2 $ quoteNeutral n e

normalize :: Type -> Term -> Term
normalize t x = quote 0 t (eval [] x)