提问人：MaiaVictor 提问时间：10/21/2023 更新时间：10/21/2023 访问量：329
是否有可能使用PHOAS将一个术语计算为正常形式，然后将其串化？
Is it possible, using PHOAS, to evaluate a term to normal form, and then stringify it?
问：
从这篇 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
这种实现允许我们创建、归一化和字符串化 λ 演算项。问题是，has type 而不是 .因此，我不清楚如何将术语评估为正常形式，然后将其字符串化。PHOAS 可能吗？evalExp t -> tExp t -> Exp t
答：
12赞
Noughtmare
10/21/2023
#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 avTerm vv ~ Term v
data FixTerm a = Fix (Term FixTerm a)
（我相信该类型与非参数 HOAS 类型同构。FixTerm
现在我们可以用它来定义我们的评估函数：
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 aVar
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)))
这次我们需要一个函数。为了能够做到这一点，我们可以在数据类型中添加一个案例，这让人想起自由的 monad 类型：v a -> FixTerm aFixTerm
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' :: Exp a -> Exp a
eval' (Exp x) = Exp (from (evalP' x))
评论
3赞
MaiaVictor
10/21/2023
这是一个写得非常好且正确的答案，谢谢。
评论
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)))) }Term v tExp t