|
[May. 7th, 2007|11:16 pm]
Jason
|
Huh, I think all this stuff about polymorphism at base types in LF is something we "already have" via a pretty simple — I'm tempted to call it "embarrassingly trivial" — embedding, one that I feel like I've implicitly seen somewhere now that I write it down. Supposing I wanted to do some nice standard thing like consing at the other end of a polymorphic list, here's some suggestive not-actually-Twelf code:
list : type -> type.
bool : type.
true : bool.
false : bool.
nil : list T.
cons : T -> list T -> list T.
snoc : list T -> T -> list T -> type.
snoc/nil : snoc nil M (cons M nil).
snoc/cons : snoc (cons N S) M (cons N S')
<- snoc S M S'.
%query 1 1 snoc (cons true (cons false nil)) true X.
Then the following code actually works in Twelf and does the right thing. The embedding consists of the declaration of t and obj, replacing every instance of type with t, and wrapping every base type with obj.
t : type.
obj : t -> type.
list : t -> t.
bool : t.
true : obj bool.
false : obj bool.
nil : obj (list T).
cons : obj T -> obj (list T) -> obj (list T).
snoc : obj (list T) -> obj T -> obj (list T) -> t.
snoc/nil : obj (snoc nil M (cons M nil)).
snoc/cons : obj (snoc (cons N S) M (cons N S'))
<- obj (snoc S M S').
%query 1 1 obj (snoc (cons true (cons false nil)) true X).
I guess some notions of glomming your whole signature into one type are usually considered dirty (at least in the absence of refinements to keep them separate), but here you really do have the type index to keep everything just as obviously adequate as before.
It's still sort of obviously bad in that it infects your whole signature, and again I'm pretty sure it's not actually a novel technique, but there might still be something to be said for the fact that the domain of the translation (i.e. LF with base-type polymorphism proper) probably has a reasonable metatheory itself. |
|
|
| Comments: |
I think you have a bug in the declaration of snoc in the top example: there is a random obj sitting there.
aha!
I was wondering what that "obj" meant, and figuring I didn't understand it. If it's a bug, suddenly I am less confused...
Yes, sorry, fixed now. It is because I obtained the first thing by copynpasting the second thing and deleting all the objs :)
I agree that this is possible now, but that we never think to do it because you're having to add an extra level to your whole encoding, which doesn't seem right. However, this is how things like Carsten's HOL-Nuprl bridge and FPCC that need an encoding of higher order logic do things: the First Five Lines of FPCC (for some value of FPCC) are: tp : type.
tm : tp -> type.
form : tp.
arrow : tp -> tp -> tp.
pf : tm form -> type. What you call obj we call tm, and we were interested in propositions ( tm form) instead of booleans ( obj bool). However, this is a highly "infectious" way of encoding things - perhaps its disfavor in the metatheorems community is unwarranted, I know I considered something like this in one early iteration of my senior thesis but either 1) wasn't smart enough at the time to sort it out or 2) just found other code examples and mimicked them or 3) got advice from Dave Walker to do it the generally-accepted way or 4) got the TALT code for primitive operations from Susmit and so legacy code won the day. The memory of which one of these it was is lost to me now.
Yeah there was a moment where I was wondering if I was just reinventing the whole "Princeton style" by accident. Writing Twelf code in the image of the translation I'm talking about does indeed seem to screw you over (or at the very least make your life hard) if you try to do any metatheory (you wind up having to prov totality of "obj", which is to say, of every meta-level function you have ever defined) but by the same token I'm pretty certain it's not HOL that I've defined.
Am I right, for instance, that FPCC defines reduction rules on the elim and intro forms of arrow?
Yes, but indirectly through the definitions lam and @ (object application), if I am understanding you correctly. The Next Six Lines of FPCC are lam : (tm T1 -> tm T2) -> tm (T1 arrow T2).
@ : tm (T1 arrow T2) -> tm T1 -> tm T2. %infix left 20 @.
imp : tm form -> tm form -> tm form. %infix right 10 imp.
forall : (tm T -> tm form) -> tm form.
beta_e : {P: tm T -> tm form} pf (P (lam F @ X)) -> pf (P (F X)).
beta_i : {P: tm T -> tm form} pf (P (F X)) -> pf (P (lam F @ X)).
Wait, so what is the notion of equality on LF terms of type (tm T)? It's some kind of Leibniz equality right?
Yes, that's precisely it... uh, I think. == : tm T -> tm T -> tm form = [a][b]
forall [P] P @ b imp P @ a. infix none 18 ==.
And yes, it's not HOL that you've defined, because you're looking in a very different direction - it's just a related representation technique. And I think the totality-of-obj was something similar to what made me give up, if that jogs my memory correctly. | |
