PHOAS.hs

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

data Ty = IntTy | FunTy Ty Ty

data Term :: (Ty -> *) -> Ty -> * where
  Lit :: Int -> Term var IntTy
  Var :: var a -> Term var a
  Add :: Term var IntTy -> Term var IntTy -> Term var IntTy
  Lam :: (var dom -> Term var ran) -> Term var (FunTy dom ran)
  App :: Term var (FunTy dom ran) -> Term var dom -> Term var ran

type Closed ty = forall var. Term var ty

type family Eval (ty :: Ty) :: * where
  Eval IntTy = Int
  Eval (FunTy fun arg) = Eval fun -> Eval arg

newtype Eval' ty = Eval' (Eval ty)

eval' :: Term Eval' ty -> Eval ty
eval' (Lit i) = i
eval' (Var (Eval' v)) = v
eval' (Add a b) = eval' a + eval' b
eval' (Lam c) = eval' . c . Eval'
eval' (App f x) = eval' f (eval' x)

eval :: Closed ty -> Eval ty
eval = eval'

type VarCounter = Int
newtype Pretty (t ::Ty) = Pretty String

nextVar :: VarCounter -> VarCounter
nextVar = (+1)

pretty' :: VarCounter -> Term Pretty ty -> String
pretty' _ (Lit i) = show i
pretty' _ (Var (Pretty v)) = v
pretty' n (Add a b) = "(" ++ pretty' n a ++ " + " ++ pretty' n b ++ ")"
pretty' n (Lam c) =
  let v = 'x' : show n in
   "(λ" ++ v ++ ". " ++ pretty' (nextVar n) (c (Pretty v)) ++ ")"
pretty' n (App f x) = pretty' n f ++ " " ++ pretty' n x

pretty :: Closed ty -> String
pretty = pretty' 0

-- Any Term with polymorphic var must be clsed.
closed_term :: Closed IntTy
closed_term = App (Lam (\v -> Add (Var v) (Lit 1))) (Lit 2)

eval_closed_term :: Int
eval_closed_term = eval closed_term

pretty_closed_term :: String
pretty_closed_term = pretty closed_term

squash :: Term (Term var) ty -> Term var ty
squash (Lit i) = Lit i
squash (Var v) = v
squash (Add a b) = Add (squash a) (squash b)
squash (Lam c) = Lam (squash . c . Var)
squash (App f x) = App (squash f) (squash x)

type Subst (t1 :: Ty) (t2 :: Ty) = forall var. var t1 -> Term var t2

subst :: Subst t1 t2 -> Closed t1 -> Closed t2
subst e1 e2 = squash (e1 e2)

my_subst :: Subst IntTy IntTy
my_subst v = Add (Var v) (Lit 3)

my_pretty :: String
my_pretty = pretty (subst my_subst closed_term)