**neelk**'s comment on my embedded DSL rant. That comment and the below-linked paper, Atkey et al.'s Unembedding domain-specific languages helped my understanding of his point a lot, so first of all, thanks much, neel.

I think I do see that what the hypothetical Haskell programmer following along with, say, section 4 of Atkey et al. is at least extraordinarily similar (and very probably isomorphic in a suitable formal sense) to what the hypothetical twelf hacker is doing when she encodes the simply-typed lambda calculus. The fact that they are doing PHOAS is good, for the 'P' ('parametric') means that many exotic programs are ruled out, though not, as they observe, the ones that use Haskell's nontermination effect. (how people are able to think of Haskell as a

*pure*functional language despite its nontotality remains a mystery to me)

But here's a bad version of the usual story: someone conceives of a domain-specific language. One considers the set X of programs in this language. One notices that there is a map f from X to Haskell, such that the intended operational semantics on X coincides exactly with the composition of f with the operational semantics of Haskell. Some work I've read, not to name names, seems to basically call it a day at this point. To repeat myself, the main trouble I have with this is that every programming library ever could have this story told about it.

The other trouble is that often the map f doesn't even seem

*full*in any sense analogous to the usual category-theoretic meaning of the word if the type system of the embedded language admits higher-order functions: there are then functions in the host language that are still quite writable, over types that are in the image of the type translation from the DSL. The action of the functor on each homset is not surjective, i.e. the translation is not full.

And therefore my DSL higher-order functionals may be called on input functions that

*do not belong*to the DSL. Have I really delineated a coherent subset that deserves to be called a new language, then? I tend to think not.

So PHOAS basically satisfies my complaint here: it at least makes the Haskell type system exactly, adequately knock out the syntax of the λ-calculus in question, modulo concerns about the host language having effects.

And for

*this*paper, despite my inclination to say that it is can without loss be described as basically being a great set of

*programming practices in Haskell*for manipulating HOAS, I think it does perhaps deserve the label of "embedding another language", because that other language really has a syntax and a static and dynamic semantics, and you can pass from the one to the other using the techniques they provide.

This is not my usual experience reading work about DSLs. I think that many of these papers try to pass under the same tent while really being a combinator library to do some particular task. Which again, I have no shortage of respect for! I just don't think it should be described by a name that confuses the issue.