Lambda the Ultimate

I am not a number: I am a free variable

Conor McBride, James McKinna

In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task in hand) and de Bruijn indices for bound variables. By doing so, we retain the advantages of both representations: naming supports easy, arithmetic-­free manipulation of terms; de Bruijn indices eliminate the need for alpha-­conversion. Further, we have ensure that not only the user but also the implementation need never deal with de Bruijn indices, except within key basic operations. Moreover, we give a representation for names which readily supports a power structure naturally reflecting the structure of the implementation. Name choice is safe and straightforward. Our technology combines easily with an approach to syntax manipulation inspired by Huet's `zippers'. Without the technology in this paper, we could not have implemented Epigram. Our example---constructing inductive elimination opera­ tors for datatype families---is but one of many where it proves invaluable.

A pretty technical paper, but fun to read.

OT: Is it just me, or the page 7 contains an easter egg? Or rather a pun...

I have a great interest in learning more about Domain Specific Languages (DSL) and how to design and implement them. So I though there is no better place to ask for this than here at LtU.

I am primarily interested in building modular language interpreters that will be embedded in other languages such as Java. So I would like to understand the basic semantic building blocks of programmming languages and then different strategies and techniques for implementing them. I am more interested on language semantics and implementation, and less on language syntax.

So if you had to recommend to me a set of books, papers, etc that could walk me through all this from beginning to end, what would that be?

Any info/references would be great.

How does one writes ß? What about λ or π or ∩ or ⊥ or ∪? Do you know all HTML entities by heart? What about mathematical symbols that do not have names, but just codes?

Assuming many browsers are Unicode-capable, should not we start using Unicode wider?

Are there any client-side Unicode helpers out there? Some dropdown that allows one to pick a symbol from a chart? A subset of couple of charts would be enough (like this one: http://www.unicode.org/charts/PDF/U2200.pdf), I don't think natural alphabets (and other non-alphabetical "natural" writing systems) should be covered.

If such utility is not readily available, and there are enough supporters of the idea, I will volunteer to do what I can.