Jason (jcreed) wrote,

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.
Tags: lf, work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded