Haskell 使用PHOAS能否将一个术语评估为正规形式然后将其转化为字符串

问题描述

根据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中是否可能实现这一点？

解决方案

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

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 数据类型添加一个情况，这种情况让人想起自由单子类型：

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