haskell - 解析PHOAS表达式

我想我了解PHOAS(参数高阶抽象语法)，
我看到了如何漂亮地打印表达式(参见http://www.reddit.com/r/haskell/comments/1mo59h/phoas_for_free_by_edward_kmett/ccbxzoo)。

但是-我看不到如何为此类表达式构建解析器，例如，它需要"(lambda (a) a)"并构建(对应的Haskell值)lam $ \ x -> x。 (并且它应该使用Text.Parsec或类似的东西。)

我可以构建一个使用de-Bruijn索引生成lambda项的解析器，但这有什么帮助？

最佳答案

正如jozefg所说，您可以轻松地在操作之间进行转换。我将展示如何在lambda术语的命名，de-Bruijn和PHOAS表示之间进行转换。如果绝对需要，将其融合到解析器中相对容易，但是最好先解析命名的表示形式然后进行转换。

假设

import Data.Map (Map)
import qualified Data.Map as M

以及lambda术语的以下三种表示形式:

基于String的名称

data LamN = VarN Name | AppN LamN LamN | AbsN Name LamN
  deriving (Eq, Show)

type Name = String

德布赖恩指数

data LamB = VarB Int | AppB LamB LamB | AbsB LamB
  deriving (Eq, Show)

菲亚斯

data LamP a = VarP a | AppP (LamP a) (LamP a) | AbsP (a -> LamP a)

现在，LamP与其他之间(双向)之间的转换。请注意，这些是部分功能。如果将它们应用于包含自由变量的lambda术语，则有责任传递合适的环境。

如何从LamN转换为LamP
将环境映射名称到
PHOAS变量。对于封闭条款，环境可以为空。

lamNtoP :: LamN -> Map Name a -> LamP a
lamNtoP (VarN n)     env = VarP (env M.! n)
lamNtoP (AppN e1 e2) env = AppP (lamNtoP e1 env) (lamNtoP e2 env)
lamNtoP (AbsN n e)   env = AbsP (\ x -> lamNtoP e (M.insert n x env))

如何从LamB转换为LamP
采用的环境是
PHOAS变量。可以是封闭条件的空白列表。

lamBtoP :: LamB -> [a] -> LamP a
lamBtoP (VarB n)     env = VarP (env !! n)
lamBtoP (AppB e1 e2) env = AppP (lamBtoP e1 env) (lamBtoP e2 env)
lamBtoP (AbsB e)     env = AbsP (\ x -> lamBtoP e (x : env))

如何从“LamP”到“LamN”

需要潜在的自由变量
实例化为其名称。为生成提供名称
活页夹的名称。应该实例化为相互之间的无限列表
不同的名字。

lamPtoN :: LamP Name -> [Name] -> LamN
lamPtoN (VarP n)         _sup  = VarN n
lamPtoN (AppP e1 e2)      sup  = AppN (lamPtoN e1 sup) (lamPtoN e2 sup)
lamPtoN (AbsP f)     (n : sup) = AbsN n (lamPtoN (f n) sup)

如何从“LamP”到“LamB”

需要潜在的自由变量
实例化为数字。采取偏移量来表示
我们目前正在使用的活页夹。应该实例化为0以关闭
术语。

lamPtoB :: LamP Int -> Int -> LamB
lamPtoB (VarP n)     off = VarB (off - n)
lamPtoB (AppP e1 e2) off = AppB (lamPtoB e1 off) (lamPtoB e2 off)
lamPtoB (AbsP f)     off = AbsB (lamPtoB (f (off + 1)) (off + 1))

一个例子

-- \ x y -> x (\ z -> z x y) y

sample :: LamN
sample = AbsN "x" (AbsN "y"
  (VarN "x" `AppN` (AbsN "z" (VarN "z" `AppN` VarN "x" `AppN` VarN "y"))
            `AppN` (VarN "y")))

通过PHOAS前往de-Bruijn:

ghci> lamPtoB (lamNtoP sample M.empty) 0
AbsB (AbsB (AppB (AppB (VarB 1) (AbsB (AppB (AppB (VarB 0) (VarB 2)) (VarB 1)))) (VarB 0)))

通过PHOAS返回名称:

ghci> lamPtoN (lamNtoP sample M.empty) [ "x" ++ show n | n <- [1..] ]
AbsN "x1" (AbsN "x2" (AppN (AppN (VarN "x1") (AbsN "x3" (AppN (AppN (VarN "x3") (VarN "x1")) (VarN "x2")))) (VarN "x2")))