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 *I***G**. 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! :-)

Can you ensure that the beta steps will terminate if there is a non-normalizable term that you are trying to type check?

Part of the trickery of dependent type checking is to only normalize terms that you have already type checked to ensure that they will terminate. I don’t see how that happens here.

augustss: My typechecker is quick and dirty and didn’t really pay attention to that concern. I have run over it once more and there are a lot of ways to improve it (mostly by tweaking the L x proofs generated). However, that last step in the derivation I showed is still staring me in the face. It must be possible to decide nonterminating terms without nonterminating!

Anyway, the system is sound, the problem is the typechecking algorithm which I naively extracted. I guess some staring is in order, to see if it can be salvaged.

Thanks for making me think.

Isn’t what you showed in the example doing some amount of type reconstruction? Just because a system is sound doesn’t mean that type reconstruction is decidable, maybe it doesn’t even mean type checking is decidable.

One more comment. If I remember right, in the extensional version of Martin-Löf type theory type checking wasn’t decidable. Proof checking was, but you needed the entire deduction tree to check it; just having the final well typed term wasn’t enough.

So finding an algorithm isn’t always possible.

Okay, I think I fixed the nontermination problems you pointed out. This is basically just a combinatory version of type theory, so typechecking won’t be decidable here either.

The trade-off, then, is that my typechecker only checks terms in normal form. That is okay for a core: advanced compilers can call this typechecker once for each normal combinator, and then again when combining. I’m working on refactoring into an interface in which this is possible and guaranteed safe.

Even though it’s less cool than the impossible claim I made earlier (a complete dependent typechecker in 100 lines), I am quite satisfied with the simplicity of this software. The “big idea” is 13 lines (and its screaming to be simplified further, I just haven’t quite seen how); the rest is just the typical LC support: AST, substitutions, quotation, etc.

Thanks again for knocking me off my impossible cloud :-)

Very interesting idea! The connection between systems with dependent types and illative combinatory logic was quite surprising for me, but some quick searching revealed it has been studied before:

– Bunder, M.W.,Dekkers, W.J.M.,Geuvers, J.H., “EQUIVALENCES BETWEEN ILLATIVE COMBINATORY LOGICS AND PURE TYPE SYSTEMS (1997)” (http://de.scientificcommons.org/35472687, http://hdl.handle.net/2433/61678);

– Bunder, M. W.,Dekkers, W. J. M., “Equivalences between Pure Type Systems and Systems of Illative Combinatory Logic (2005)” (http://de.scientificcommons.org/933015)

(Unfortunately, only the earlier paper seems to be freely accessible online.)

I have also a question: in the paper you cite, there is a remark ((iv), page 18) that the systems described are actually based on lambda calculus, but could be reformulated to variable-free combinatory versions. Maybe such a reformulation could further simplify your implementation?

Doesn’t type checking only terms in normal form make it very limiting? I mean, the point of running code is to normalize it, so before running it, it’s not normalized.

Also, dependent type checking usually needs to interleave normalization with type checking. Some of the definitions you have need to be unfolded to make things type check. How would that work with checking one combinator at a time?