haskell 有没有可能，使用PHOAS，将一个术语评估为标准形式，然后将其字符串化？

qcbq4gxm 于 2023-11-18 发布在其他

关注(0)|答案(1)|浏览(105)

从this Haskell Cafe post，并借用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可以吗？

haskell

来源：https://stackoverflow.com/questions/77332495/is-it-possible-using-phoas-to-evaluate-a-term-to-normal-form-and-then-stringi

1条答案

按热度按时间

kyvafyod1#

让我们从最幼稚的事情开始：

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

型

赞(0）回复(0）举报 2023-11-18

我来回答

haskell 有没有可能，使用PHOAS，将一个术语评估为标准形式，然后将其字符串化？

1条答案

相关问题

热门标签

最新问答