[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
Frank Atanassow
franka at cs.uu.nl
Fri Aug 13 20:05:55 EDT 2004
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
More information about the Haskell-Cafe
mailing list