Type Specialisation

Here is an introductory paper on type specialisation, from the Glasgow workshop last year. It contains more or less the same material as the first lecture on the subject.

However, this paper doesn't describe the concrete syntax that the implemented specialiser processes. The best way to learn that, and to get a feel for what type specialisation can achieve, is to work through the following demo. One clarification: you'll notice that the only dynamic constructors introduced in the demo are Inl and Inr; other constructor names (such as Cons, Nil etc) refer to static constructors. That's because Inl and Inr are the only dynamic constructors implemented -- sorry. You will need to represent all dynamic sums either using them, or the specialisable constructor In. You'll also notice that no strings are used in the demo. They aren't implemented either, which is why the interpreter presented uses integers as variable names.

The last example in the demo is an interpreter for the lambda-calculus. Copy it to a file, and carry out the following exercises. Rather than run the specialiser on our web server, you can run it locally: it's

~rjmh/ImpPE/Main

1. Modify the interpreter so that calls of eval are unfolded rather than specialised, and make sure (on at least the two examples in the demo) that you obtain optimal specialisations. (This version of the type specialised post-processes beta-redexes into lets: optimal specialisation means equal programs modulo this post-processing).
2. Modify the interpreter further into continuation passing style. Verify that you obtain optimal CPS conversion by specialising it now (cf Exercise 3).
3. Returning to the interpreter of part 1, change the representation of interpreted functions to use static functions instead of dynamic ones. This makes the definition of a function one of its static properties, with the consequence that only one function may be bound to each function variable -- bad news for higher-order functions. But using specialisable constructors you can lift that restriction. Using this idea, develop a typed closure conversion, which converts any lambda-expression into an essentially first-order program.