[Haskell-cafe] closed classes

[Peter G. Hancock]

> At the moment I'm only thinking of parameter-less kind declarations but
> one could easily imagine kind parameters, and soon we'll have kind
> polymorphism....  but one step at a time.

> Any thoughts?  

Apologies if it's widely known, but a system with "kind polymorphism"
was first considered by Girard (in 1971!).  It's mentioned in Appendix A
of "The System F of Variable Types, Fifteen Years Later" by Girard in
"Logical Foundations of Functional Programming", ed Huet,
Addison-Wesley 1990, pp 87-126.  There he calls it "system U".  

It is inconsistent, and non-normalising (as a logical system).  The
implications of this for type-checking "should be considered very
cautiously" (to borrow Girard's words).

Peter Hancock