解析PHOAS表达式

Question

我想我理解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项的解析器,但它会有什么帮助呢？

Answer 1

正如jozefg所说,您可以轻松地在操作之间进行转换.我将展示如何在命名,de-Bruijn和lambda术语的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

de-Bruijn指数

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

PHOAS

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

Answer 2

jozefg在他的评论中有正确的答案.总是解析为一个简单的抽象语法树,而不是一些聪明的表示.然后,在解析之后,转换表示.在这种情况下,很容易

data Named = NLam String Named | NVar String | NApp Named Named

convert :: (String -> a) -> Named -> Exp a a
convert f (NVar n) = var $ f n
convert f (NApp e1 e2) = app (convert f e1) (convert f e2)
convert f (NLam s e) = lam $ \a -> convert (nf a) e where
  nf a s' = if s' == s then a else f s'

你当然可以使用除函数之外的其他东西String -> a作为你的地图. Data.Map例如,将摆脱线性时间查找.

与其他HOAS方案相比,PHOAS的一个很酷的事情是你可以轻松"转换回"

addNames :: ExpF Int (State Int Named) -> State Int Named
addNames (App a b) = liftM2 NApp a b
addNames (Lam f)   = do
  i <- get
  put (i + 1)
  r <- f i
  return $ NLam ('x':show i) r

convert' :: Exp Int Int -> Named
convert' = fst 
  . flip runState 0
  . cata addNames 
  . liftM (return . NVar . ('x':) . show)

甚至按预期工作

?: convert' $ convert undefined $ NLam "x" $ NApp (NVar "x") (NLam "y" (NVar "y"))
> NLam "x0" (NApp (NVar "x0") (NLam "x1" (NVar "x1")))