[TYPES] Universe Polymorphism

[Sebastian Hanowski]

* Am 22.06.08 schrieb Klaus Ostermann:

> In  particular  I  am  interested in  practical  (maybe  implemented?)
> programming languages  which support an infinite  number of universes,
> some notion of "type:type", or  other interesting features along these
> lines.

Have a look at:

        http://www.cs.nott.ac.uk/~txa/publ/pisigma.pdf

        http://sneezy.cs.nott.ac.uk/cgi-bin/PiSigma

> What are the practical implications of having "type:type"? I read that
> it destroys the consistency of the type system as a logic, but this is
> not  relevant  for  my  purposes.  On  one  hand,  I  have  read  that
> type-checking in systems with "type:type" is not decidable, but on the
> other hand, the paper "Why dependent  types matter" mentions in Sec. 7
> that the authors  have adopted "type:type" in  their Epigram language.
> How does this  fit together? Are there any useful  examples in Epigram
> (or any other language) that use the "type:type" possibility?

"Type:Type"  is  not part  of  the  design  of the  Epigram  programming
language.  Foundational issues  with  polymorphic stratified  universes,
postponed design  decisions and  a prototypical  implementation probably
all can count in why it is present in the Epigram 1 system.
For an outlook into the future see:

        http://article.gmane.org/gmane.comp.lang.epigram/167

And this  an 'idiomatic'  Epigram program showing  universe polymorphism
beeing desirable,  which in the meantime  is only possible with  the *:*
shortcut:

        http://sneezy.cs.nott.ac.uk/epigram/durham/examples/ctm/veczip.epi


Cheers,
Sebastian