Lambda the Ultimate

Putting Curry Howard to Work

The Curry­Howard isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this prob­lem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new fea­tures are backward compatible with existing features, and combine to enable a new programming paradigm for functional program­mers. This paradigm makes it possible to state and enforce interest­ing properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.

A new paper by Tim Sheard showing us "language features of the future".

In Haskell (as implemented in GHC and Hugs with extensions), you can use type-classes to construct a type equality (either a fully generic one in GHC or a type level equivalent of the Typeable datatype for Hugs). Using type level equality, you can remove overlapping instances from multi-parameter-type-classes with functional-dependancies. This allows you to write arbitrary (although non-backtracking) type level logic programs using type constraints, which construct functional programs as their output.

As an example of how far you can go with this - look at the code Joy.hs distributed with the HList library, it is a type-level implementation of the language Joy in Haskell's type system.

The only problem here is that the type-level language cannot make proof judgments about itself, only about the language being "typed". (This is because types in the "typed" language become values in the meta-language). This means you might nead a meta-meta level etc...

It seems that this can be flattened to a single language if you allow Types == Values (and presumably Kinds would also be values). One possible result of making types and values equivalent is that the type-system becomes the main programming language and you end up with an untyped logic language (say Prolog, note that prolog is still 'kinded' in that facts must have that same 'arity' to be considered for unification)...

The alternative would be a fully type inferenced dependantly typed functional language (obviously explicit constraints would be given not inferred, but they can be given by constraining functions avoiding the need for the programmer to ever explicitly give types)... Martin Lof's Type Theory seems suited as a type system for this sort of language.

I just wanted to point out that the work linked here is Emir Pasalic's Ph.D. thesis: Emir was Tim Sheard's student, so Tim was definitely involved, and the thesis does in some sense pre-figure Ωmega. But I think we should also give Emir some credit here, especially if the topic name is taken from his (directly linked) dissertation. Perhaps you could edit the original comment to reflect this, just as a courtesy?

Meta-programming is programming at compile-time. Why is there a need to differenciate between compile-time programs and run-time programs? both are programs executed by a computer. The fact that one program is used to produce another program does not make it any different than the run-time portion producing data to be fed to yet another running program.

The available meta-Java and meta-C++ solutions already prove that one does not need special support for meta-programming.

We should not forget the great work of Hongwei Xi and his students.
e.p.

I finally started reading this thesis a couple of days ago (I didn't find it via this post, but indirectly via a comment Paul made here). It's one of the best things I've read in a long time - a very gentle introduction to a whole pile of interesting topics. If you're someone like me (ie not part of the whole academic scene, but with some background in Haskell and not too scared by a very small amount of formal semantics) then I would *strongly* recommend this.

At the risk of too much self-linking I even copied a section out and posted it here - it's talking about staged interpreters rather than GADTs, but I think it gives a good taste of the style (and illustrates an interesting point that stands alone).

Seriously; this guy should write a textbook.