After an inquiry about a combinatory calculus for dependent types, somebody in #haskell — unfortunately I don’t remember who — recommended I look at Illative Combinatory Logic. After studying the paper a bit, all I can say is Wow! It implements a (conjecturally) complete logical system in but three simple typing rules, together with the untyped lambda calculus conversion rules. I was able to write a dependent typechecker in 100 lines.
The specific system I’m working with in the paper is called system IG. The paper also introduces three weaker systems, which are also very nice and worth understanding.
As an example, here is a derivation of the identity function and its type. This is a backward proof, so each step is implied by the step after it. But reading it this way makes the algorithm clear.
|- G L (\A. G A (\_. A)) (\A x. x) L a |- (\A. G A (\_. A)) a ((\A x. x) a) (Gi) L a |- G a (\_. a) ((\A x. x) a) (beta) L a |- G a (\_. a) (\x. x) (beta) L a, a b |- (\_. a) b ((\x. x) b) (Gi) L a, a b |- a ((\x. x) b) (beta) L a, a b |- a b (beta)
The trick, which isn’t so much a trick as a beautiful deep connection I gather (although I don’t fully grok it), is that typing propositions are just applications. So if A is a type, then A b is the proposition “b has type A”. L is the type of types, and G is essentially Π (the product type constructor). So, for example, the fourth line in the above proof would be written as follows in a conventional system:
a : Type |- (\x. x) : a -> a
I need to extend it with finite types and boxes, but I really don’t want to because it’s so pretty as is! :-)