Parametric higher order syntax (PHOAS) for simply typed lambda calculus

PHOAS.hs

{-# LANGUAGE RankNTypes, TypeApplications, DataKinds, KindSignatures, GADTs, TypeFamilies #-}

-- 1. Parametric higher order abstract syntax (PHOAS) of untyped lambda calculus
--------------------
data PTerm p = Var p | Lam (p -> PTerm p) | App (PTerm p) (PTerm p)
type Term = forall p . PTerm p

-- A semantic domain
data Dom = Embed { retract :: Dom -> Dom }

interp :: Term -> Dom
interp t = go t where
  go :: PTerm Dom -> Dom
  go (Var d) = d
  go (Lam f) = Embed (go . f)
  go (App f x) = retract (go f) (go x)


-- 2. Type safe syntax tree of simply typed lambda calculus
-----------------------------

-- Types of a simply typed lambda calculus
data Ty = BoolTy | Arrow Ty Ty

-- 2.1 Terms with De Bruijn indices
data Env = Nil | Cons Ty Env

data Index (t :: Ty) (env :: Env) where
  ZeroIdx :: Index t (Cons t Nil)
  SuccIdx :: Index t env -> Index t (Cons t' env)

data TermTyped (ctx :: Env) (t :: Ty) where
  VarTyped :: Index t env -> TermTyped env t
  LamTyped :: TermTyped (Cons a env) t -> TermTyped env (Arrow a t)
  AppTyped :: TermTyped env (Arrow a b) -> TermTyped env a -> TermTyped env b

-- 2.2 Terms in PHOAS

-- Parametric higher order syntax tree for a simply typed lambda calculus
data PTermTyped (i :: Ty -> *) (t :: Ty) where
  Var' :: i t -> PTermTyped i t
  Lam' :: (i a -> PTermTyped i b) -> PTermTyped i (Arrow a b)
  App' :: PTermTyped i (Arrow a b) -> PTermTyped i a -> PTermTyped i b

-- Close terms
type TermTyped' t = forall (i :: Ty -> *) . PTermTyped i t

-- An example of a term
t1 :: TermTyped' (Arrow (Arrow BoolTy BoolTy) (Arrow BoolTy BoolTy))
t1 = Lam' (\f -> Lam' (\x -> Var' f `App'` (Var' f `App'` Var' x)))

type family Interp (t :: Ty) :: * where
  Interp BoolTy = Bool
  Interp (Arrow a b) = Interp a -> Interp b

-- Type families cannot be partially applied
newtype WrapInterp t = WrapInterp { unwrap :: Interp t }

interp' :: TermTyped' t -> Interp t
interp' t = unwrap (go t) where
  go :: PTermTyped WrapInterp t -> WrapInterp t
  go (Var' x) = x
  go (Lam' f) = WrapInterp (unwrap . go . f . WrapInterp)
  go (App' a b) = WrapInterp ((unwrap (go a)) (unwrap (go b)))

-- interp' t1 :: (Bool -> Bool) -> Bool -> Bool 
test = interp' t1 not True