Differences between HOAS and FOAS
abstract-syntax-tree, haskell
Solution
jozefg's answer explains what FOAS and HOAS is, so in this answer, I just try to answer the various smaller points from the question. Read jozefg's answer first, I guess.
What about the While constructor makes it HOAS?
Let's look at the second argument of the `While` constructor: `While :: ... -> (FunC s -> FunC s) -> ...`. In the type of this field, `FunC` shows up to the left of an arrow. So if you use `While` in a `FunC` program, your program is not an abstract syntax tree in memory, but something more complicated. The intended meaning of `FunC s -> FunC s` is "a `FunC s` with a free variable of type `s`". I guess this is used for the body of a while loop, and the free variable contains the value that changes in each loop iteration.
Why are none of the other constructors HOAS?
They don't have the `... -> (FunC ... -> ...) -> ...` pattern we saw with the `While` constructor above. So if a `FunC` value only uses the other constructors, its memory representation looks like an abstract syntax tree.
Again, I don't understand what makes the data defined in HOAS.hs HOAS while the data defined in FOASTyped is FOAS.
You can look at the FOAS version of the code in the paper to see how they change the type of `While` to avoid the HOAS pattern, and what else they need to change to make it work.
Is there some general way in which HOAS is more difficult to transform than FOAS?
A HOAS program is not a tree, so you cannot pattern match on it. For example, you cannot pattern match on `While (\_ _ (LitB False)) ...` because you cannot match on lambdas like this.
How does HOAS help with type safety compared to FOAS?
In a HOAS program, you use Haskell variables to represent `FunC` variables. The Haskell typechecker will check that you only use Haskell variables in the scope of a corresponding variable binding. (GHC tells you "Not in scope: `foo'`" otherwise). Because `FunC` variables are represented as Haskell variables, this check is also useful for the type safety of `FunC`. If you use a HOAS-encoded `FunC` variable out of scope, the Haskell typechecker will complain about the Haskell variable being out of scope.
Now in FOAS, if you use Haskell Strings as FunC variables, the Haskell type checker will never complain if you use the wrong string, because you can use whatever string you want as far as GHC is concerned. There are techniques for improving FOAS to make the Haskell typechecker check your embedded program, but they tend to require more work from the user of the embedded language.
What is a variable binder?
A variable binder is 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 introduce a new name `x` that I can use in the `...`. Other binders in Haskell include lambda expressions, pattern matching, and top-level definitions.
how does Haskell implement it?
I don't really get this question. For typechecking, GHC keeps track of what variables are in scope where and complains if you use variables at the wrong place. For compilation, GHC generates machine code that "knows" where the values denoted by the variables are, usually because a pointer to the value of the variable is stored in a processor register or the stack or the heap.
and what languages don't have variable binders?
Many small and specialized languages don't have variable binders.
For example, consider regular expressions. At least originally, they cannot bind variables. (Some regular expression engines use backreferences, which are a form of variables, though).
Another example is the "language" of URLs. A URL is made of various parts (the protocol, server name, path, parameters, ...) with rules about what you can and cannot write, so it is a language. But you cannot introduce a name in a URL that you can later use in the URL.
Many low-level languages don't have variable binders.
- For example, x86 machine code contains just numbers, no names.
There are Turing-complete languages without variable binders.
- For example, the SK calculus.
Problem
In trying to decide if a EDSL is prudent for my project, I read this paper and this paper, describing the implementation of meta-repa. They both mention HOAS and FOAS. From the first paper, ``` 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`. What about the `While` constructor makes it HOAS? Why are none of the other constructors HOAS? In the second paper, meta-repa code is written in a HOAS tree, then transformed (at compile-time) to a FOAS for further processing. Again, I don't understand what makes the data defined in HOAS.hs HOAS while the data defined in FOASTyped is FOAS. The mysterious quote from that paper is: 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. Is there some general way in which HOAS is more difficult to transform than FOAS? How does HOAS help with type safety compared to FOAS? I've read the Wikipedia article on FOAS and HOAS, but that didn't clear anything up for 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 what languages don't have variable binders?