February 26th, 2008

beartato phd

(no subject)

neelk prodded me to write a short note about an idea I had last spring. The idea was that polymorphism in LF a la Nanevski-Morrisett-Birkedal can be fruitfully special-cased to just base-type polymorphism, in which type variables can be instantiated with base types, not arbitrary (i.e. function) types. Nonetheless you get to quantify over type operators as higher-order as you wish, which puts the system is in some bizarro limbo-zone with respect to the λ-cube. Anyway it simplifies the definition of LF in a couple of ways, since you no longer need to mention a signature separate from the context, since the context is now allowed to invent types and type families, (which behave just as well as they used to — the lesson here being that to hypothesize an unknown type in Twelf is not practically different from hypothesizing an unknown base type — we never do anything that would distinguish the two) and the type and term levels collapse nicely in a couple places.

I posted to livejournal back when it first occurred to me, but I don't think I ever described the really cute thing about it, which is that you can write higher-order functions like map in logic-programming style with kind
(A → B → type) → (list A) → (list B) → type
(see how it's taking an entire predicate as its first argument?) and with a simple hack you can get them to run (although you can't reason about them usefully) in Twelf. Surely this has been thought of before in a less type-disciplined setting? Dunno. That's what I expect from the Prolog community anyway.