Simple dependently typed evaluator

Bwd.hs

module Bwd where

data Bwd a = Empty
           | Bwd a :> a

instance Functor Bwd where
  fmap f Empty = Empty
  fmap f (xs :> x) = fmap f xs :> f x

instance Eq a => Eq (Bwd a) where
  Empty == Empty = True
  (xs :> x) == (ys :> y) = (xs == ys) && x == y
  _ == _ = False

deriving instance Show a => Show (Bwd a)

instance Foldable Bwd where
  foldMap f Empty = mempty
  foldMap f (xs :> x) = foldMap f xs <> f x

instance Traversable Bwd where
  traverse f Empty = pure Empty
  traverse f (xs :> x) = (:>) <$> traverse f xs <*> f x

hd :: Bwd a -> a
hd (_ :> x) = x

tl :: Bwd a -> Bwd a
tl (xs :> _) = xs

nth :: Int -> Bwd a -> a
nth 0 (xs :> x) = x
nth i (xs :> x) = nth (i - 1) xs

fromList :: [a] -> Bwd a
fromList = foldl (\acc x -> acc :> x) Empty

toList :: Bwd a -> [a]
toList = foldr (:) []

Simple.hs

module Simple where

import Bwd

data Tms
  = Idt
  | Comp Tms Tms
  | Epsilon
  | TCons Tms Tm
  | Fst Tms
  deriving (Show)

data Tm
  = Snd Tms
  | Sub Tm Tms
  | Lam Tm
  | App Tm
  | ElU
  | ElPi Tm Tm
  | ElSig Tm Tm
  | ElUnit
  | Pair Tm Tm
  | Proj1 Tm
  | Proj2 Tm
  | Constant
  deriving (Show)

tm_app :: Tm -> Tm -> Tm
tm_app f u = Sub (App f) (TCons Idt u)

class Repr a where
  repr :: a -> Tm

instance Repr Int where
  repr 0 = Snd Idt
  repr n = Sub (repr (n-1)) (Fst Idt)

data Val
  = Susp Int (Bwd XElim)
  | Clos (Val -> Val)
  | VU
  | VPi Val (Val -> Val)
  | VSig Val (Val -> Val)
  | VUnit
  | VPair Val Val
  | VConstant

data XElim
  = XApp Val
  | XProj1
  | XProj2

type Env = Bwd Val

eval :: Tm -> Env -> Val
eval (Snd s) p = hd (evals s p)
eval (Sub u s) p = eval u (evals s p)
eval (Lam u) p = Clos (\v -> eval u (p :> v))
eval (App u) (p :> v) = apply (eval u p) v
eval ElU p = VU
eval (ElPi a b) p = VPi (eval a p) (\v -> eval b (p :> v))
eval (ElSig a b) p = VSig (eval a p) (\v -> eval b (p :> v))
eval ElUnit p = VUnit
eval (Pair a b) p = VPair (eval a p) (eval b p)
eval (Proj1 u) p = proj1 (eval u p)
eval (Proj2 u) p = proj2 (eval u p)
eval Constant p = VConstant

evals :: Tms -> Env -> Env
evals Idt p = p
evals (Comp s w) p = evals s (evals w p)
evals Epsilon p = Empty
evals (TCons s u) p = (evals s p) :> (eval u p)
evals (Fst s) p = tl (evals s p)

apply :: Val -> Val -> Val
apply (Clos f) v = f v
apply (Susp h e) v = Susp h (e :> XApp v)

proj1 :: Val -> Val
proj1 (VPair t u) = t
proj1 (Susp h e) = Susp h (e :> XProj1)

proj2 :: Val -> Val
proj2 (VPair t u) = u
proj2 (Susp h e) = Susp h (e :> XProj2)

data Nf
  = Neu Int (Bwd Elim)
  | NLam Nf
  | NU
  | NPi Nf Nf
  | NSig Nf Nf
  | NUnit
  | NPair Nf Nf
  | NConstant
  deriving (Show, Eq)

data Elim
  = EApp Nf 
  | EProj1
  | EProj2
  deriving (Show, Eq)

instance Repr Nf where
  repr (Neu h e) = foldl repr_apply (repr h) e
  repr (NLam f) = Lam (repr f)
  repr NU = ElU
  repr (NPi a b) = ElPi (repr a) (repr b)
  repr (NSig a b) = ElSig (repr a) (repr b)
  repr NUnit = ElUnit
  repr (NPair a b) = Pair (repr a) (repr b)
  repr NConstant = Constant

repr_apply :: Tm -> Elim -> Tm
repr_apply t (EApp u) = tm_app t (repr u)
repr_apply t EProj1 = Proj1 t
repr_apply t EProj2 = Proj2 t

quote :: Int -> Val -> Nf
quote d (Susp h e) = Neu (d - h - 1)
                         (fmap (quote_elim d) e)
quote d (Clos f) = NLam (quote (d+1) (f (Susp d Empty)))
quote d VU = NU
quote d (VPi a b) = NPi (quote d a)
                        (quote (d+1) (b (Susp d Empty)))
quote d (VSig a b) = NSig (quote d a)
                          (quote (d+1) (b (Susp d Empty)))
quote d VUnit = NUnit
quote d (VPair a b) = NPair (quote d a) (quote d b)
quote d VConstant = NConstant

quote_elim :: Int -> XElim -> Elim
quote_elim d (XApp u) = EApp (quote d u)
quote_elim d XProj1 = EProj1
quote_elim d XProj2 = EProj2

idenv :: Int -> Env
idenv 0 = Empty
idenv n = idenv (n-1) :> Susp (n-1) Empty