Thread by @rob_rix

@a_cowley Pattern matching on the argument to the higher-order function is definitely a mistake, which PHOAS resolves by making it impossible. Learned that one the hard way!

@a_cowley Additionally, the basic treatment of it as e.g.:

data Expr = App Expr Expr | Lam (Expr -> Expr)

doesn’t really allow for free variables, which you often want—e.g. distinguishing locals, represented by variables in the metalanguage, from globals, represented as a constructor.

@a_cowley That can also be used to allow you to “quote” the thing back to a first-order representation, for equality tests, pretty-printing, etc. But I tend to use strings for var names in my term syntax, and then how do you know you’re not going to be clobbering other names?

@a_cowley 1. Lexical scoping means that’s not a problem unless/until you’re substituting in the first-order syntax, but substituting in first-order syntax has the usual capture avoidance challenges anyway; so why do it?
2. My Name datatype has a Gensym constructor so I can use Ints.

@a_cowley Finally, there’s the problem of actually constructing the things since you have to do so in pure code; (Expr -> Expr) doesn’t leave room for effects. So while my eval function runs in a Reader, it does the actual recursive evaluation in a pure function which it passes the env.

@a_cowley I also define substitution of globals in my HOAS Value type so that I can make, and then substitute, fresh names during unification, applying the higher-order functions to the fresh var, and then recovering a higher-order function by substituting the var with the arg.

@a_cowley Just about the only thing my current representation *doesn’t* offer is the ability to explicitly represent conflicts in the structure so I can easily do Elm-style type diffing for error messages. Thinking of doing this by splitting Expr into ExprF a and two different fixpoints.