HOAS 和 FOAS 之间的区别

Question

HOAS 和 FOAS 之间的区别

7

在我试图决定是否在我的项目中使用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

We have also chosen Higher Order Abstract Syntax to represent constructs with variable binding. In the above data type, the only higher-order construct is While.

什么让While构造函数成为了HOAS？为什么其他构造函数都不是HOAS？

在第二篇论文中，meta-repa代码写在一个HOAS树中，然后（在编译时）转换为FOAS以进行进一步处理。同样，我不明白在HOAS.hs中定义的数据是如何成为HOAS而在FOASTyped中定义的数据则是FOAS。来自那篇论文的神秘引用如下：

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

是否存在一些通用的方法，使HOAS比FOAS更难转换？与FOAS相比，HOAS如何帮助实现类型安全？

我已经阅读了FOAS和HOAS的维基百科文章，但这并没有为我澄清任何问题。

维基百科认为HOAS在具有“变量绑定器”的语言中很有用（也在第一个引用中提到）。什么是变量绑定器，Haskell如何实现它，哪些语言没有变量绑定器？

- crockeea

2个回答

7

jozefg的回答解释了FOAS和HOAS是什么，因此在这个回答中，我只尝试回答问题中的各种较小点。我想先阅读jozefg的答案。

While构造函数中的哪个部分使其成为HOAS？

让我们看一下While构造函数的第二个参数：While :: ... -> (FunC s -> FunC s) -> ...。在此字段的类型中，FunC出现在箭头的左侧。因此，如果您在FunC程序中使用While，则您的程序不是内存中的抽象语法树，而是更复杂的东西。 FunC s -> FunC s的预期含义是“具有类型为s的自由变量的FunC s”。我猜这是用于while循环的主体，自由变量包含每个循环迭代中发生更改的值。

为什么其他构造函数都不是HOAS？

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

同样，我不明白HOAS.hs中定义的数据是如何成为HOAS，而FOASTyped中定义的数据则是FOAS。

您可以查看论文中的FOAS版本代码，了解它们如何更改While的类型以避免HOAS模式，以及他们需要改变什么才能使其工作。

是否有一种通用的方式，HOAS比FOAS更难转换？

HOAS程序不是一棵树，因此您无法对其进行模式匹配。例如，您无法对While (\_ _ (LitB False)) ...进行模式匹配，因为您无法像这样匹配lambda。

与FOAS相比，HOAS如何帮助实现类型安全？

在HOAS程序中，您使用Haskell变量来表示FunC变量。 Haskell类型检查器将检查您是否仅在相应变量绑定的范围内使用Haskell变量。（否则GHC会告诉您“未定义：foo'”）。因为FunC变量被表示为Haskell变量，所以这个检查对于FunC的类型安全也很有用。如果您在作用域之外使用HOAS编码的FunC变量，则Haskell类型检查器将抱怨Haskell变量超出了范围。

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

“什么是变量绑定？”

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

“Haskell如何实现它？”

我真的不明白这个问题。对于类型检查，GHC跟踪哪些变量在哪里处于作用域，并在您在错误的位置使用变量时发出警告。对于编译，GHC生成“知道”变量表示的值在哪里的机器代码，通常因为指向变量值的指针存储在处理器寄存器、堆栈或堆中。

“哪些语言没有变量绑定器？”

许多小型和专业化语言没有变量绑定器。

例如，考虑正则表达式。至少最初，它们不能绑定变量。(一些正则表达式引擎使用反向引用，这是一种变量形式，但不是所有)。

另一个例子是URL的“语言”。URL由各种部分(协议、服务器名称、路径、参数等)组成，有关您可以和不能写入的规则，因此它是一种语言。但是，您无法在URL中介绍一个名称，然后稍后在URL中使用它。

许多低级语言没有变量绑定器。

例如，x86机器码只包含数字，没有名称。

还有一些没有变量绑定器的图灵完备语言。

例如，SK演算。

- Toxaris

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Daniel Gratzer · Accepted Answer

在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中，我们必须确保正确地进行α转换，以确保我们正确地尊重作用域。这个优势同样适用于所有绑定变量（variable-binders）的事物：Let表达式、continuations, 异常处理程序等等。

然而，这也带来了一个主要的缺点，因为Lam具有完全抽象的函数，我们无法检查函数体。这使得很多转换非常困难，因为一切都被Haskell绑定包裹起来。

另一个好处是，由于我们不为变量提供显式构造器，所有术语都保证关闭。

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