- Proposes a small syntactic extension to the lambda calculus.
- Gives an intuition for how it works and some equivalent, lambda-only constructions.
- Gives an operational semantics.
- Proves the soundness and completeness of a simple type system.
- Proves the soundness and completeness of a parametrically polymorphic type system.
- Designs and proves correct several optimizations for this construct.
- Lists compelling use cases for the new extension.
- Provides an evaluation of the extension as applied to one of those use cases.
I’ve seen a lot of papers which are only the first three, or perhaps four or five. But the last three items are the real kicker. They show that Shivers is really grounded, that he’s not just rambling about Foozles, but is interested in making programming languages better.
If there’s any problem, it’s his writing and way of explaining. Shivers has worked alone a lot, for some unsurprising reasons, so his prose clearly reflects a single person’s thoughts. On the one hand, this makes reading his work a little difficult; on the other, it’s probably the source of a lot of his creativity and incision.