haskell - HOAS 和 FOAS 的区别

Question

在尝试确定 EDSL 是否适合我的项目时，我阅读了 this paper和 this paper ，描述元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 code写在 HOAS 树中，然后(在编译时)转换为 FOAS 以进行进一步处理。同样，我不明白是什么让 HOAS.hs HOAS 中定义的数据，而 FOASTyped 中定义的数据是 FOAS。那篇论文的神秘引语是:

The type Expr [in HOAS.hs] uses higher order abstract syntax to represent programs. This representation is convenient for programming with but somewhat less ideal for rewriting programs. The AST is therefore converted into a first order representation[.] A possible implementation would have been to skip the [HOAS] Expr type and generate the first order representation directly. We have kept the higher order representation partly because it helps maintain the type safety of the implementation and partly because it allows us to write a well typed, tagless interpreter.

HOAS 是否比 FOAS 更难转换？与 FOAS 相比，HOAS 对类型安全有何帮助？

我已经阅读了关于 FOAS 和 HOAS 的 Wikipedia 文章，但这并没有为我解决任何问题。

Wikipedia 建议 HOAS 在具有可变绑定(bind)器的语言中很有用(在第一个引用中也提到过)。什么是变量绑定(bind)器，Haskell 是如何实现的，哪些语言没有变量绑定(bind)器？

Answer 1

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

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

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

我们有明确的变量，现在由我们来确保范围和变量绑定(bind)正常工作。然而，额外的工作是有返回的，因为我们现在可以在 lambda 的主体上检查和模式匹配，这对于大多数转换至关重要。

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

例如，考虑 STLC

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

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

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

它有效。在正常的 AST 中，我们必须确保我们正确地对所有内容进行 alpha 转换，以确保我们正确地尊重范围。同样的优势适用于所有绑定(bind)变量(变量绑定(bind)器)的东西:让表达式、延续、异常处理程序等等。

不过，这有一个主要缺点，因为 Lam有一个完全抽象的函数，我们根本无法检查函数体。这使得很多转换都很好，很痛苦，因为一切都被包裹在 Haskell 绑定(bind)之下。

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

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