[POPLmark] [Provers] Re: Adequacy for LF

[Frank Pfenning]

> 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?

Yes, this is the intent and the basic intuition for
its design.  - Frank