A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions
by Brigitte Pientka, appeared in POPL 08.
Higher-order abstract syntax (HOAS) is a simple, powerful technique
for implementing object languages, since it directly supports
common and tricky routines dealing with variables, such as
capture-avoiding substitution and renaming. This is achieved by
representing binders in the object-language via binders in the meta-language.
However, enriching functional programming languages
with direct support for HOAS has been a major challenge, because
recursion over HOAS encodings requires one to traverse -
abstractions and necessitates programming with open objects.
We present a novel type-theoretic foundation based on contextual
modal types which allows us to recursively analyze open terms
via higher-order pattern matching. By design, variables occurring
in open terms can never escape their scope. Using several examples,
we demonstrate that our framework provides a name-safe foundation
to operations typically found in nominal systems. In contrast
to nominal systems however, we also support capture-avoiding
substitution operations and even provide first-class substitutions to
the programmer. The main contribution of this paper is a syntax directed
bi-directional type system where we distinguish between
the data language and the computation language together with the
progress and preservation proof for our language.
Its been a while since I posted, but this paper appears that it may be of interest to some members of this community. It looks interesting to me, but I just wish I understood all the terminology. I don't know what "open objects" are, and why they are a problem. I don't understand what HOAS is. I don't even know what binders are. The list goes on. I surely can't be the only person who is interested, but feels that this is just out of their grasp. I bet that I probably could understand these things with a minimum of explanation, given I have experience implementing languages. If anyone is interested in rephrasing the abstract in more basic terms, I would be very appreciative.
[Edit: corrected spelling of Brigitte Pientka. My apologies.]