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

Question

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

11

从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中是否可能实现这个功能？

- MaiaVictor

我的第一个想法是通过评估来进行规范化，这应该可以与HOAS一起使用——例如，

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 t和Exp t。 - undefined

Dolio 在 Agda 中实现了这个功能：https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda - undefined

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Noughtmare · Accepted Answer

让我们从尝试最简单的方法开始吧：

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，所以现在我们知道我们应该选择包含 Term v 的 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 数据类型中添加一个与自由单子类型类似的情况。

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