Jason (jcreed) wrote,
Jason
jcreed

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
Subscribe

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 9 comments