20

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

4

3 回答 3

22

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

PHOAS

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

现在是 LampP 和其他人之间的转换（双向）。请注意，这些是偏函数。如果您将它们应用于包含自由变量的 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")))
于 2013-10-17T07:09:13.577 回答
6

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")))
于 2013-10-17T06:30:55.477 回答
3

我将再次以此处其他答案的主题运行，并建议您进行解析，就好像您只是在使用命名变量创建天真的表示。如果您想避免中间表示，您可以将其内联到解析器中，而不会使其更难理解：

data Lam a = Var a | Lam a `App` Lam a | Lam (a -> Lam a)

type MkLam a = (String -> a) -> Lam a

var :: String -> MkLam a
var x = Var . ($ x)

app :: MkLam a -> MkLam a -> MkLam a
app = liftA2 App

lam :: String -> MkLam a -> MkLam a
lam v e env = Lam $ \x -> e $ \v' -> if v == v' then x else env v'

这个想法是，您无需在解析器中使用中间表示的构造函数，而是直接使用这些函数。它们具有与构造函数相同的类型，因此它实际上只是一个替代品。它也有点短，因为现在我们不必单独写出 ADT 和解释器。

于 2013-10-23T04:00:31.920 回答