That line of thought also lead me off on a tangent with an old idea that I keep returning to occasionally, namely how to push thinking of LF in spine form just a little further to appropriately coalesce not just sequences of arguments, but sequences of λs as well. It turns out, I think, that putting the whole calculus 'in substitution form' instead of 'in spine form', is the way to do it. Basically it looks a lot like CMTT, except without the 'M', and every variable is contextual: function types themselves are realized in "lowered" fashion. I write them as Π-types, but basically they are much more like the types (Ψ |- A) from CMTT. The consequence is that many of the syntactic productions collapse in a lovely way, even more so if I also lump in the ideas I had a while ago about polymorphism restricted to base types. In deBruijn form all that remains of the entire syntax of the language is:
Natural Numbers n ::= 0, 1, 2, ...
Atomic Classifiers a ::= type | R
Atomic Terms R ::= n[σ]
Classifiers V ::= ΠΨ.a
Normal Terms N ::= λnR
Substitutions σ ::= id | N.σ
Contexts Γ,Ψ ::= . | Γ,A
That's it! No signature necessary because you can do it all in the context, (although I reckon an implementation would still want a signature for pragmatic reasons, to avoid deBruijn-shift renumberings of frequently-used constants) no unnecessary syntactic distinction between terms and types, and types and kinds, you get some of the laziness benefits of explicit substitutions, and you get a limited form of type operators and polymorphism almost for free.
In the afternoon I went over to the Embassy party, saw some awesome folks, some of which don't usually appear in pittsburgh any more such as damion and theadana and fizzbang.
After that jra1279 appeared with her boyfriend Andy, after some crazy pittsburgh highway hassle, here being en route for them on their way eventually to Milwaukee. It was awesome to finally meet the two of them! We had dinner at JM's and chatted for a while before they headed back to the road.