Differences between HOAS and FOAS

Question

When trying to decide whether EDSL is reasonable for my project, I read this article and this article describing the implementation of meta-rep. They both mention HOAS and FOAS. From the first article

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 also chose a higher order abstract syntax to represent a variable-bound construct. In the above data type, the higher order construction is While .

What about the While constructor making it HOAS? Why none of the other HOAS constructors?

In the second document, the metadata code is written to the HOAS tree and then converted (at compile time) to FOAS for further processing. Again, I do not understand what the data defined in HOAS.hs HOAS does, while the data defined in FOASTyped is FOAS. Mysterious quote from this article:

The Expr type [in HOAS.hs] uses a higher order abstract syntax to represent programs. This view is convenient for programming, but somewhat less ideal for rewriting programs. Therefore, AST is converted to a first-order representation [.] A possible implementation would be to skip the [HOAS] Expr and directly form a first-order representation. We retained a higher order view, partly because it helps maintain the security type of the implementation, and partly because it allows us to write a well-typed, carefree interpreter.

Is there some general way in which HOAS is harder to convert than FOAS? How does HOAS help with type safety compared to FOAS?

I read a Wikipedia article about FOAS and HOAS, but that didn't explain anything to me.

Wikipedia suggests that HOAS is useful in languages ​​with variable binders (also mentioned in the first quote). What is a variable binder, how does Haskell implement it, and which languages ​​do not have variable binders?

Answer 1

Jozefg's answer explains what FOAS and HOAS are, so in this answer I'm just trying to answer various smaller questions from the question. First try answering jozefg.

As for the constructor, while making it a HOAS?

Let's look at the second argument to the While constructor: While :: ... -> (FunC s -> FunC s) -> ... In the type of this field, FunC displayed to the left of the arrow. Therefore, if you use While in a FunC program, your program is not an abstract syntax tree in memory, but something more complex. The supposed meaning of FunC s -> FunC s : "a FunC s with a free variable of type s ". I assume this is used for the body of the while loop, and the free variable contains a value that changes in each iteration of the loop.

Why none of the other HOAS constructors?

They do not have a template ... -> (FunC ... -> ...) -> ... , which we saw using the While constructor above. Therefore, if the FunC value uses only other constructors, its memory representation looks like an abstract syntax tree.

Again, I don't understand what the data defined in HOAS.hs HOAS does, whereas the data defined in FOASTyped is FOAS.

You can look at the version of the FOAS code in the document to see how they change the While type to avoid the HOAS pattern, and what else needs to be changed to make it work.

Is there some general way in which HOAS is harder to convert than FOAS?

HOAS is not a tree, so you cannot map a pattern. For example, you cannot match pattern matching on While (\_ _ (LitB False)) ... because you cannot match it with lambdas.

How does HOAS help with type safety compared to FOAS?

HOAS uses Haskell variables to represent FunC variables. The Haskell controller verifies that you use only Haskell variables in the binding area of ​​the corresponding variable. (The GHC tells you "Not in scope: foo' " otherwise). Because FunC variables FunC represented as Haskell variables, this check is also useful for security like FunC . If you use the FunC -dependent FunC variable, a Haskell value will complain that the Haskell variable is out of scope.

Now in FOAS, if you use Haskell Strings as FunC variables, a Haskell type checker will never complain if you use the wrong string, because you can use any string that you need with respect to GHC. There are FOAS enhancement methods to get Haskell typechecker to check your firmware, but they usually require more work from the user of the embedded language.

What is a variable binder?

Variable binding is a language construct that introduces new names that you can use in other parts of the program. For example, in Haskell, if I write let x = 14 in ... , I will introduce a new name x , which I can use in ... Other binders at Haskell include lambda expressions, pattern matching, and top-level definitions.

How does Haskell implement it?

I really don't ask this question. For type checking, the GHC keeps track of which variables are in the area, where it complains if you use the variables in the wrong place. For compilation, the GHC generates machine code that “knows” where the values ​​indicated by the variables are usually related to the fact that the pointer to the value of the variable is stored in the processor register or on the stack or on the heap.

and which languages ​​do not have variable binders?

Many small and specialized languages ​​do not have variable binders.

• For example, consider regular expressions . At least initially they cannot bind variables. (Some regex engines use backreferences, which are a form of variables, though).

• Another example is the "language" of a URL . The URL consists of various parts (protocol, server name, path, parameters, etc.) with rules on what you can and cannot write, therefore it is a language. But you cannot enter a name in the URL, which can later be used in the URL.

Many low-level languages ​​do not have variable binders.

• For example, x86 machine code contains only numbers, without names.

There are language versions of Turing without variable binders.

• For example, costing SK .

Answer 2

In FOAS, we represent variables with identifiers, so

  data STLC = Var String | Lam String STLC | Unit | STLC :*: STLC term = Lam "a" $ Lam "b" $ Var "a" :*: (Lam "a" $ Var "a") 

We have explicit variables, and now we can make sure that the scope binding and the variable are working correctly. However, the extra work has its advantages, because we can now check and compare samples throughout the lambda body, which is vital for most transformations.

HOAS is essentially where we use the implementation of host language variables (Haskell) instead of representing them in AST.

For example, consider STLC

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

Notice how we use the Haskell STLC -> STLC to represent a variable associated with a lambda. That means we can write

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

and it works. In a regular AST, we need to make sure that we alpha-convert everything correctly to ensure that we properly evaluate visibility. The same advantage applies to all things that bind variables (binding variables): let expressions, continuations, exception handlers, whatever.

This is due to a serious flaw, since Lam has a completely abstract function, we cannot generally check the body of the function. This makes a lot of transformations well, painfully, as everything is wrapped under a Haskell binding.

Another advantage is that since we do not provide an explicit constructor for variables, all members are guaranteed to be private.

This usually means that we present things with a combination of HOAS and FOAS.