Lambda the Ultimate

Last year, Ehud said the only reason he missed the Scala Lift Off was because it didn't have enough marketing. So this year I'm spam^h^h^h^h posting it on the LtU front page.

The Scala Lift Off San Francisco will be held on Saturday, June 6th in San Francisco. This is the Saturday after JavaOne. Admission to the event is $200. If you are a full time student or faculty member, the cost is $50. We'll have hot and cold running food and beverages, improved wifi, and lots of terrific members of the Scala and Lift community.

Further details and registration are at the conference site. I'll add comments to this topic as more information becomes available.

This blog post about Idris led me to Edwin C. Brady's 2005 PhD thesis, Practical Implementation of a Dependently Typed Functional Programming Language.

This thesis considers the practical implementation of a dependently typed programming language, using the Epigram notation defined by McBride and McKinna. Epigram is a high level notation for dependently typed functional programming elaborating to a core type theory based on Luo's UTT, using Dybjer's inductive families and elimination rules to implement pattern matching. This gives us a rich framework for reasoning about programs. However, a naive implementation introduces several run-time overheads since the type system blurs the distinction between types and values; these overheads include the duplication of values, and the storage of redundant information and explicit proofs.

A practical implementation of any programming language should be as efficient as possible; in this thesis we see how the apparent efficiency problems of dependently typed programming can be overcome and that in many cases the richer type information allows us to apply optimisations which are not directly available in traditional languages. I introduce three storage optimisations on inductive families; forcing, detagging and collapsing. I further introduce a compilation scheme from the core type theory to G-machine code, including a pattern matching compiler for elimination rules and a compilation scheme for efficient runtime implementation of Peano's natural numbers. We also see some low level optimisations for removal of identity functions, unused arguments and impossible case branches. As a result, we see that a dependent type theory is an effective base on which to build a feasible programming language.

What's the current state of the art in optimization of dependently typed languages?