[Haskell-cafe] closed classes
Peter G. Hancock
hancock at spamcop.net
Mon Aug 9 13:01:06 EDT 2004
> 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).
More information about the Haskell-Cafe