[POPLmark] [Provers] Re: Adequacy for LF

[Frank Pfenning]

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.  One reason is that it would completely alter
the nature of all the internal analyses and the would be much harder to
prove correct and to trust.  The other reason is that there is much less
need for it than in ordinary programming.  Lists are a convenient data
structure with simple types, but with dependent types there are often
much better ways to represent data so that we can capture internal
invariants.

For example, you might think of a (linear) computation as a list of
states, or a list of steps.  But is much better to represent it as

id : red* S S.
;  : red* S1 S2 -> red* S2 S3 -> red* S1 S3.
step : red S1 S2 -> red* S1 S2.

or

id : red* S S.
step : red S1 S2 -> red* S2 S3 -> red* S1 S3.

because the dependent types give you adequacy on valid transition
sequences which you do not capture in a list.  I have observed this
frequently, and I don't think it is specific to LF/Twelf, but probably
applies to dependent types in general.

Polymorphic data structures are "blind": the very fact that they are
parametrically polymorphic means that they don't capture any property of
the underlying data.

As Karl hinted, the module system will also certainly help to alleviate
the lack of polymorphism by allowing you to instantiate generic modules.
And, no, I don't know when this will be available.

As for functions, that is a slippery slope.  Carsten Schuermann, Joelle
Despeyroux and I worked out what kind of modal type system would be
required to allowing mixing of higher-order syntax with total functions
defined by cases and recursion.  It was a worthwhile exercise, but I
don't think it turned out to be very usable.  Carsten's more recent work
on Delphin (where you have a much stronger separation of levels) may be
the answer, depending on what kind of functions you had in mind.

  - Frank

> From:    Greg Morrisett <greg at eecs.harvard.edu>
> ...
> I've been disappointed by the apparent lack of "polymorphism"
> in Twelf -- I seem to have to define various kinds of lists at
> every level.  For someone used to coding instead of proving,
> that's painful.  Is there a way around this?
> 
> And finally, I find it somewhat annoying that when
> I write a simple, total function, I have to step out to the
> meta-level to establish that it is indeed a function.
> Maybe there's a good way around this too?
> 
> -Greg