Is it possible, using PHOAS, to evaluate a term to normal form, and then stringify it?

Question

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?

My first thought was normalisation by evaluation, which should work with HOAS—for example, class Norm t where { unquote :: Term t -> t; quote :: t -> Term t }; instance (Norm a, Norm b) => Norm (a -> b) where { unquote f = x -> unquote (App f (quote x)); quote f = Lam (x -> quote (f (unquote (Var x)))) }. But I don’t immediately see how to deal with your polymorphic Term v t and Exp t. — 9 hours ago
Dolio implemented this in Agda: hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda — 5 hours ago

score 6 · Accepted Answer · 2023-10-20 21:45:43Z

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))

This is an extremely well written and correct answer, thank you. — 4 hours ago

Is it possible, using PHOAS, to evaluate a term to normal form, and then stringify it?