
9 Aug
2004
9 Aug
'04
5:01 p.m.
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