PHOAS.hs

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

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

type family Subst var (vs :: [Ty]) (ty :: Ty) = r | r -> var vs ty where
  Subst var '[] ty = Term (Term var) ty
  Subst var (v:vs) ty = Term var v -> Subst var vs ty

type Open vs ty = forall var. Subst var vs ty

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)

subst :: Open (v:vs) ty -> Closed v -> Open vs ty
subst e1 e2 = e1 e2

close :: Open '[] ty -> Closed ty
close = squash

my_subst :: Open [IntTy, IntTy] IntTy
my_subst v1 v2 = Add (Var v1) (Var v2)

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