[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]

[Frank Atanassow]

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