From this Haskell Cafe post, and borrowing some code examples from jyp, we can construct a simple PHOAS evaluator in Haskell as:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Data.Char
data Term v t where
Var :: v t -> Term v t
App :: Term v (a -> b) -> Term v a -> Term v b
Lam :: (v a -> Term v b) -> Term v (a -> b)
data Exp t = Exp (forall v. Term v t)
-- An evaluator
eval :: Exp t -> t
eval (Exp e) = evalP e
data Id a = Id {fromId :: a}
evalP :: Term Id t -> t
evalP (Var (Id a)) = a
evalP (App e1 e2) = evalP e1 $ evalP e2
evalP (Lam f) = \a -> evalP (f (Id a))
data K t a = K t
showTermGo :: Int -> Term (K Int) t -> String
showTermGo _ (Var (K i)) = "x" ++ show i
showTermGo d (App f x) = "(" ++ showTermGo d f ++ " " ++ showTermGo d x ++ ")"
showTermGo d (Lam a) = "@x" ++ show d ++ " " ++ showTermGo (d+1) (a (K d))
showTerm :: Exp t -> String
showTerm (Exp e) = showTermGo 0 e
This implementation allows us to create, normalize and stringify λ-calculus terms. The problem is, eval
has type Exp t -> t
rather than Exp t -> Exp t
. As such, it isn't clear to me how to evaluate a term to normal form, and then stringify it. Is that possible with PHOAS?
Let's start by trying the most naive thing:
evalP' :: Term v a -> Term v a
evalP' (Var x) = Var x
evalP' (App x y) =
case (evalP' x, evalP' y) of
(Lam f, y') -> f (_ y')
(x', y') -> App x' y'
evalP' (Lam f) = Lam (evalP' . f)
We get stuck at that hole because we need a function Term v a -> v a
, so now we know that we should chose the v
such that it contains Term v
. We can chose v ~ Term v
, but you can't use recursive types directly like that so you need to create a new data type:
data FixTerm a = Fix (Term FixTerm a)
(I believe the FixTerm
type is isomorphic to the non-parametric HOAS type.)
Now we can use that to define our evaluation function:
evalP' :: Term FixTerm a -> Term FixTerm a
evalP' (Var (Fix x)) = evalP' x
evalP' (App x y) =
case (evalP' x, evalP' y) of
(Lam f, y') -> f (Fix y')
(x', y') -> App x' y'
evalP' (Lam f) = Lam (evalP' . f)
This works, but unfortunately we can't recover the original Term v a
from this. It's easy to see that because it never produces a Var
constructor. We can again try and see where we get stuck:
from :: Term FixTerm a -> Term v a
from (Var (Fix x)) = from x
from (App x y) = App (from x) (from y)
from (Lam f) = Lam (\x -> from (f (_ x)))
This time we need a function v a -> FixTerm a
. To be able to do that we can add a case to the FixTerm
data type, which is reminiscent of the free monad type:
data FreeTerm v a = Pure (v a) | Free (Term (FreeTerm v) a)
evalP' :: Term (FreeTerm v) a -> Term (FreeTerm v) a
evalP' (Var (Pure x)) = Var (Pure x)
evalP' (Var (Free x)) = evalP' x
evalP' (App x y) =
case (evalP' x, evalP' y) of
(Lam f, y') -> f (Free y')
(x', y') -> App x' y'
evalP' (Lam f) = Lam (evalP' . f)
from :: Term (FreeTerm v) a -> Term v a
from (Var (Pure x)) = Var x
from (Var (Free x)) = from x
from (App x y) = App (from x) (from y)
from (Lam f) = Lam (\x -> from (f (Pure x)))
Now we can define the top-level eval:
eval' :: Exp a -> Exp a
eval' (Exp x) = Exp (from (evalP' x))