[POPLmark] [Provers] Re: Adequacy for LF

[Greg Morrisett]

Frank Pfenning wrote:
> Parametric polymorphism could be added to Twelf (in fact, earlier
> version of Elf had this as an undocumented feature), but I have
> steadfastly resisted it.  

Your point regarding polymorphism & dependency is well-taken.

I'm not sure the "polymorphism" is the right term for what
I'm looking for.  Rather, I need some abstraction mechanisms that
keep me from writing so much boiler-plate.  For instance,
I clearly want lists at the level of syntax for things
like lists of declarations, lists of expressions, and lists
of (object-level) types (perhaps because there's no dependency
at this level.)

I'd be perfectly happy if there was a meta-level facility for generating
the specializations of these definitions.  For one thing, having to come
up with n different names for "cons" is well, painful :-)

I can get this (for syntax) by essentially making a single
universe for all my syntactic objects, and then build the
appropriate well-formedness conditions separately.  But
this extra level of indirection is pretty painful in practice.

Maybe this is the sort of thing the module system will
provide support for?

-Greg