August 5th, 2007

beartato phd

(no subject)

Quite some time ago, (probably on several separate occasions, actually) Frank mentioned to me the possibility of having dependently-typed contexts where dependencies are cyclic — but he treated it as an idea fairly high up on the craziness scale.

However, I think I figured out how to make it work. Here are some somewhat brief notes on how the system looks and an outline of the correctness proofs. The key is that asserting that everything is simply-typed from the get-go lets us be fairly reckless with carrying out some crazy hereditary substitutions that are not generally going to be fully dependently well-typed (because we at least know they will all normalize, thanks to the simple types), and just check, after the dust settles, that all the indices match up.

As a consequence the system has Πs powerful enough to abstract over even cyclically dependent collections of free unification variables that arise from examples like the one I posted here. As for implementation details, I think you might just use deBruijn indices that are integers instead of natural numbers.