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

Question

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

\n

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE RankNTypes #-}\n\nimport Data.Char\n\ndata Term v t where\n   Var :: v t -> Term v t\n   App :: Term v (a -> b) -> Term v a -> Term v b\n   Lam :: (v a -> Term v b) -> Term v (a -> b)\n\ndata Exp t = Exp (forall v. Term v t)\n\n-- An evaluator\neval :: Exp t -> t\neval (Exp e) = evalP e\n\ndata Id a = Id {fromId :: a}\n\nevalP :: Term Id t -> t\nevalP (Var (Id a)) = a\nevalP (App e1 e2)  = evalP e1 $ evalP e2\nevalP (Lam f)      = \\a -> evalP (f (Id a))\n\ndata K t a = K t\n\nshowTermGo :: Int -> Term (K Int) t -> String\nshowTermGo _ (Var (K i)) = "x" ++ show i\nshowTermGo d (App f x)   = "(" ++ showTermGo d f ++ " " ++ showTermGo d x ++ ")"\nshowTermGo d (Lam a)     = "@x" ++ show d ++ " " ++ showTermGo (d+1) (a (K d))\n\nshowTerm :: Exp t -> String\nshowTerm (Exp e) = showTermGo 0 e\n

\n

此实现允许我们创建、规范化和字符串化 \xce\xbb-演算项。问题是，eval有类型Exp t -> t而不是Exp t -> Exp t。因此，我不清楚如何将术语评估为正常形式，然后将其字符串化。PHOAS 可以做到这一点吗？

\n

Answer 1

让我们从尝试最天真的事情开始：

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)

我们陷入了这个洞，因为我们需要一个函数Term v a -> v a，所以现在我们知道我们应该选择v它包含的函数Term v。我们可以选择v ~ Term v，但是你不能像这样直接使用递归类型，所以你需要创建一个新的数据类型：

data FixTerm a = Fix (Term FixTerm a)

（我相信该FixTerm类型与非参数 HOAS 类型同构。）

现在我们可以用它来定义我们的评估函数：

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)

这可行，但不幸的是我们无法Term v a从中恢复原始内容。很容易看出这一点，因为它从不生成Var构造函数。我们可以再次尝试看看我们被困在哪里：

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

这次我们需要一个函数v a -> FixTerm a。为了能够做到这一点，我们可以向FixTerm数据类型添加一个 case，这让人想起自由 monad 类型：

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

现在我们可以定义顶级 eval：

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