On Aug 9, 2004, at 5:00 PM, Simon Peyton-Jones wrote:
Closed classes are certainly interesting, but a better way to go in this case is to allow the programmer to declear new kinds, as well as new types. This is what Tim Sheard's language Omega lets you do, and I'm considering adding it to GHC.
FWIW, Martin Wehr designed a Haskell-like type system with: * not only datakinds, but datasuperkinds, datasupersuperkinds, etc., in short, data-n-types for every finite dimension n, all parametric, * along with parametrically polykinded, polysuperkinded, etc., in short, poly-n-morphic functions, * along with map, simple folds and nested folds for all these things, * not to mention an algorithm for principal type inference in his 1998 paper: @misc{ wehr98higher, author = "M. Wehr", title = "Higher order algebraic data types", text = "Martin Wehr. Higher order algebraic data types (full paper). Technical report, University of Edinburgh, URL http://www.dcs.ed.ac.uk/home/wehr, July 1998.", year = "1998", url = "citeseer.nj.nec.com/wehr98higher.html" } The title of the paper is a bit misleading: "higher-dimensional" is better than "higher-order", as higher-order functions are the chief thing missing from Wehr's system. But these are easily added in the standard fashion, which is to say, only at the value level, and by simply neglecting the problem of defining folds for datatypes involving (->). Two significant differences between Wehr's system and the one Simon described is that every kind in Wehr's system has values, and there is no distinguished kind *. I tried to champion this (very incoherently) in a talk at the Hugs/GHC meeting in, I think, 2000, where Tim also presented some of his early ideas on datakinds. (BTW, given such an expressive system, I think you may find, as I did, that the number of ways to represent what amount to essentially the same type grows ridiculously large, and this is one of the motivations for treating more general notions of type equivalence than equality, like for example canonical isomorphy as I am doing in a forthcoming paper.) There is also an extended abstract of Wehr's paper in CTCS (no citation handy---I'm posting this from at home), and a categorical semantics which is, however, not for the faint of heart: @article{ wehr99higherdimensional, author = "Martin Wehr", title = "Higher-dimensional syntax", journal = "Electronic Notes in Theoretical Computer Science", volume = 29, year = 1999, url = "citeseer.nj.nec.com/wehr99higher.html" } Eelco Visser also defines a notion of multi-level type system, and gives several examples of how they can be used, in his PhD thesis. One of the examples, as I recall, shows how datakinds and polykinded functions subsume uni-parameter type classes (without overlapping instances). Regards, Frank