是否可以使用 PHOAS 将术语评估为范式，然后将其字符串化？

Question

从 this Haskell Cafe 帖子，并借用 jyp 中的一些代码示例，我们可以在 Haskell 中构造一个简单的 PHOAS 求值器：

{-# 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

此实现允许我们创建、规范化和字符串化 λ 演算项。问题是，

eval

的类型是

Exp t -> t

而不是

Exp t -> Exp t

。因此，我不清楚如何将术语评估为正常形式，然后将其字符串化。 PHOAS 可以做到这一点吗？

Answer 1

您可以通过一种免费的 monad 构造来做到这一点：

data FreeTerm v t = Pure (v t) | Free (Term (FreeTerm v) t)

eval' :: Exp a -> Exp a
eval' (Exp x) = Exp (from (evalP' (Free x)))

evalP' :: FreeTerm v a -> FreeTerm v a
evalP' (Free (Var x)) = evalP' x
evalP' (Free (App e1 e2)) =
  case (evalP' (Free e1), evalP' (Free e2)) of
    (Free (Lam f), e2') -> Free (f e2')
    (e1', e2') -> Free (App (unfree e1') (unfree e2'))
evalP' (Free (Lam f)) = Free (Lam (unfree . evalP' . Free . f))
evalP' (Pure x) = Pure x

unfree :: FreeTerm v t -> Term (FreeTerm v) t
unfree (Pure x) = Var (Pure x)
unfree (Free x) = x

from :: FreeTerm v a -> Term v a
from (Pure x) = Var x
from (Free (Var x)) = from x
from (Free (App e1 e2)) = App (from (Free e1)) (from (Free e2))
from (Free (Lam f)) = Lam (\x -> from (Free (f (Pure x))))