HOAS和FOAS之间的差异

Question

在试图判断EDSL是否对我的项目是谨慎的时候,我阅读了本文和本文,描述了meta-repa的实现.他们都提到了HOAS和FOAS.从第一篇论文,

 data FunC a where
  LitI :: Int -> FunC Int
  LitB :: Bool -> FunC Bool
  If :: FunC Bool -> FunC a -> FunC a -> FunC a
  While :: (FunC s -> s -> FunC Bool) -> (FunC s -> FunC s) 
                -> FunC s -> FunC s
  Pair :: FunC a -> FunC b -> FunC (a, b)
  Fst :: FunC (a, b) -> FunC a
  Snd :: FunC (a, b) -> FunC b
  Prim1 :: String -> (a -> b) -> FunC a -> FunC b
  Prim2 :: String -> (a -> b -> c) -> FunC a -> FunC b -> FunC c
  Value :: a -> FunC a
  Variable :: String -> FunC a

我们还选择了高阶抽象语法来表示具有变量绑定的构造.在上面的数据类型中,唯一的高阶构造是While.

怎么样的While构造函数使它成为HOAS？为什么其他建设者都没有HOAS？

在第二篇论文中,元修复代码在HOAS树中编写,然后(在编译时)转换为FOAS以进行进一步处理.同样,我不明白在HOAS.hs HOAS中定义数据的原因是什么,而FOASTyped中定义的数据是FOAS.该论文的神秘引言是:

Expr[HOAS.hs]中的类型使用更高阶的抽象语法来表示程序.这种表示对于编程很方便,但对于重写程序来说有点不太理想.因此,AST被转换为一阶表示[.]可能的实现是跳过[HOAS] Expr类型并直接生成第一阶表示.我们保留了更高阶的表示,部分原因是它有助于维护实现的类型安全性,部分原因是它允许我们编写一个良好类型的无标记解释器.

是否有一些通用的方式使HOAS比FOAS更难改造？与FOAS相比,HOAS如何帮助确保类型安全？

我已经阅读了有关FOAS和HOAS的维基百科文章,但这对我来说并不清楚.

维基百科建议HOAS在具有可变绑定器的语言中很有用(在第一个引用中也提到过).什么是变量绑定器,Haskell如何实现它,以及哪些语言没有可变绑定器？

Answer 1

在FOAS中,我们用标识符表示变量,所以

 data STLC = Var String
           | Lam String STLC
           | Unit
           | STLC :*: STLC

 term = Lam "a" $
        Lam "b" $
        Var "a" :*: (Lam "a" $ Var "a")

我们有明确的变量,现在由我们来确保范围和变量绑定正常工作.额外的工作有它的奖励,因为我们现在可以检查和模式匹配lambda的身体,这对大多数转型至关重要.

HOAS本质上是我们使用宿主语言(Haskell)实现变量而不是在AST中表示它们的地方.

例如,考虑STLC

  data STLC = Unit
            | Lam (STLC -> STLC)
            | STLC :*: STLC

注意我们如何使用Haskell函数STLC -> STLC来表示由lambda绑定的变量.这意味着我们可以写

  term = Lam $ \a ->
         Lam $ \b ->
         a :*: (Lam $ \a -> a)

它的工作原理.在正常的AST中,我们必须确保我们正确地对所有内容进行alpha转换,以确保我们正确地遵守范围.同样的优点适用于绑定变量(变量绑定器)的所有事情:让表达式,连续性,异常处理程序,等等.

这有一个主要的缺点,因为Lam有一个完全抽象的功能,我们根本无法检查功能的主体.这使得很多转换很好,很痛苦,因为一切都在Haskell绑定下完成.

另一个好处是,由于我们没有为变量提供显式构造函数,因此所有术语都保证关闭.

通常这意味着我们用HOAS和FOAS的组合来表示事物.

Answer 2

jozefg的答案解释了FOAS和HOAS是什么,所以在这个答案中,我只是试着回答问题中的各个较小点.我想,首先阅读jozefg的答案.

那么While构造函数使它成为HOAS？

让我们看一下While构造函数的第二个参数:While :: ... -> (FunC s -> FunC s) -> ....在此字段的类型中,FunC显示在箭头的左侧.因此,如果您While在FunC程序中使用,您的程序不是内存中的抽象语法树,而是更复杂的东西.意图FunC s -> FunC s是" FunC s具有类型的自由变量s".我想这用于while循环的主体,而free变量包含在每次循环迭代中更改的值.

为什么其他建设者都没有HOAS？

它们没有... -> (FunC ... -> ...) -> ...我们在While上面的构造函数中看到的模式.因此,如果FunC值仅使用其他构造函数,则其内存表示看起来像抽象语法树.

同样,我不明白在HOAS.hs HOAS中定义数据的原因是什么,而FOASTyped中定义的数据是FOAS.

您可以查看论文中代码的FOAS版本,了解它们如何更改类型While以避免HOAS模式,以及需要更改以使其工作的其他内容.

是否有一些通用的方式使HOAS比FOAS更难改造？

HOAS程序不是树,因此您无法对其进行模式匹配.例如,你不能模式匹配,While (\_ _ (LitB False)) ...因为你不能匹配像这样的lambdas.

与FOAS相比,HOAS如何帮助确保类型安全？

在HOAS程序中,您使用Haskell变量来表示FunC变量.Haskell类型检查器将检查您是否仅在相应的变量绑定范围内使用Haskell变量.(GHC告诉你"不在范围内:foo'"否则).因为FunC变量表示为Haskell变量,所以此检查对于类型安全性也很有用FunC.如果你使用HOAS编码的FunC变量超出范围,Haskell类型检查器会抱怨Haskell变量超出范围.

现在在FOAS中,如果你使用Haskell字符串作为FunC变量,如果使用错误的字符串,Haskell类型检查器将永远不会抱怨,因为就GHC而言,你可以使用你想要的任何字符串.有一些技术可以改进FOAS以使Haskell类型检查器检查您的嵌入式程序,但它们往往需要嵌入式语言用户的更多工作.

什么是可变粘合剂？

变量绑定器是一种语言结构,它引入了可以在程序的其他部分中使用的新名称.例如,在Haskell中,如果我写,let x = 14 in ...我会引入一个x我可以使用的新名称....Haskell中的其他绑定器包括lambda表达式,模式匹配和顶级定义.

Haskell如何实现它？

我真的不明白这个问题.对于类型检查,GHC会跟踪哪些变量在范围内,如果在错误的位置使用变量,则会抱怨.对于编译,GHC生成的机器代码"知道"变量表示的值的位置,通常是因为指向变量值的指针存储在处理器寄存器或堆栈或堆中.

什么语言没有变量粘合剂？

许多小型和专业语言没有可变绑定器.

• 例如,考虑正则表达式.至少最初,他们无法绑定变量.(一些正则表达式引擎使用反向引用,但这是一种变量形式).

• 另一个例子是URL的"语言" .URL由各种部分(协议,服务器名称,路径,参数......)组成,其中包含有关您可以写和不可写的内容的规则,因此它是一种语言.但是,您无法在URL中引入名称,以后可以在URL中使用该名称.

许多低级语言没有可变绑定器.

• 例如,x86机器代码只包含数字,没有名称.

有图灵完整语言没有可变绑定器.

• 例如,SK演算.