RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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. kind HNat = HZero | HSucc HNat class HNatC (a::HNat) instance HNatC HZero instance HNatC n => HNatC (HSucc n) Here the keyword 'kind' is like 'data', except that it introduces a new *kind* HNat with new *type* constructors HZero and HSucc, rather than a new *type* constructor with new *data* constructors. There is no way to construct a value of type HZero, or (HSucc HZero); these are simply phantom types. Today we are forced to say data HNat data HSucc a which loses the connection between the two. A merit of declaring a kind is that the kind is closed -- the only types of kind HNat are HZero, HSucc HZero, and so on. So the class doesn't need to be closed; no one can add new instances to HNatC because they don't have any more types of kind HNat. 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? Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of | Duncan Coutts | Sent: 06 August 2004 15:11 | To: MR K P SCHUPKE | Cc: Haskell Cafe | Subject: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either] | | On Fri, 2004-08-06 at 14:05, MR K P SCHUPKE wrote: | > >You should include the definitions of the classes before saying | > | > HOrderedList l' just has to prove by induction that for any element | > in the list, the next element is greater, so the class is simply: | > | > class HOrderedList l | > instance HNil | > instance HCons a HNil | > instance (HOrderedList (HCons b l),HLe a b) => HCons a (HCons b l) | | Somewhat off-topic, | | It's when we write classes like these that closed classes would be | really useful. | | You really don't want people to add extra instances to this class, it'd | really mess up your proofs! | | I come across this occasionally, like when modelling external type | systems. For example the Win32 registry or GConf have a simple type | system, you can store a fixed number of different primitive types and in | the case of GConf, pairs and lists of these primitive types. This can be | modelled with a couple type classes and a bunch of instances. However | this type system is not extensible so it'd be nice if code outside the | defining module could not interfere with it. | | The class being closed might also allow fewer dictionaries and so better | run time performance. | | It would also have an effect on overlapping instances. In my GConf | example you can in particular store Strings and lists of any primitive | type. But now these two overlap because a String is a list. However | these don't really overlap because Char is not one of the primitive | types so we could never get instances of String in two different ways. | But because the class is open the compiler can't see that, someone could | always add an instance for Char in another module. If the class were | closed they couldn't and the compiler could look at all the instances in | deciding if any of them overlap. | | So here's my wishlist item: | | closed class GConfValue v where | ... | | Duncan | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi On Mon, 9 Aug 2004, 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.
kind HNat = HZero | HSucc HNat
class HNatC (a::HNat)
instance HNatC HZero instance HNatC n => HNatC (HSucc n)
[..]
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?
Yes. "Yes please." This is still in the realm of using type-level proxies for values, but it's a much more practical fake of dependent types than you can manage with type classes. It lets you do quite a lot of the handy indexing that's found in basic dependently typed programs, without quite crossing the line to full-on value dependency. Of course, I recommend crossing this line in the long run, but I accept that doing so might well mess things up for GHC. This is a sensible, plausible step in the right direction. And I'm sure you'll be able to jack it up to datakinds parametrized by datakinds, provided all the indices are in constructor form: the unification apparatus you've already got for datatype families (or GADTs as you've dubbed them) should do everything you need, as long as you unify the indices before you unify the indexed `values'. What you still don't get is the ability to use datatype families to reflect on values in order to extend pattern matching, the way James McKinna and I do in `The view from the left'. But one step at a time. You also don't get for free the ability to write type-level programs over these things. If you do add type-level programs over datakinds, you may find that the unification-in-the-typing-rules style comes under strain. I'm told that's why the ALF crew retreated from full-on datatype families, which is why they're not in Cayenne. The Epigram approach is different: the unification problems are solved internally to the theory, so you still get the solutions when they're easy, but the wheels don't come off when they're not. Even so, you do get quite a long way towards the `static' uses of dependent types which support n-ary vectors and the like, but where n isn't supposed to be a run-time value. You'll get `projection from a vector is exception-free'; you won't get `projection from a vector returns the thing in that position in the vector'. So let's have this, and we'll see how many of the programs I've written in the last 5+ years with these data structures become Haskell programs. More than a few, I expect. Cheers Conor
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
On Mon, Aug 09, 2004 at 04:00:44PM +0100, Simon Peyton-Jones wrote:
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?
My first thought is I am going to need a better editor mode that can tell from context whether an identifier is a value, type, or kind (or meta-kind?) constructor and differentiate them visually :) would these kind constructors need to be encoded into system F or the lambda cube, or would it be possible that they be eliminated right after typechecking or easily desugared away like classes? The idea is quite interesting. I was thinking about explicit kinds the other day, but just as an idle curiosity, now that this thread has provided some real-world interesting uses, I will have to think about them some more :) John -- John Meacham - ⑆repetae.net⑆john⑈
Simon Peyton-Jones wrote:
kind HNat = HZero | HSucc HNat
class HNatC (a::HNat)
instance HNatC HZero instance HNatC n => HNatC (HSucc n)
There is no way to construct a value of type HZero, or (HSucc HZero); these are simply phantom types. ... A merit of declaring a kind is that the kind is closed -- the only types of kind HNat are HZero, HSucc HZero, and so on. So the class doesn't need to be closed; no one can add new instances to HNatC because they don't have any more types of kind HNat.
With the flag -fallow-overlapping-instances, could I still add an instance instance HNatC n => HNatC (HSucc (HSucc n)) or instance HNatC (HSucc HZero) ?? If I may I'd like to second the proposal for closed classes. In some sense, we already have them -- well, semi-closed. Functional dependencies is the way to close the world somewhat. If we have a class class Foo x y | x -> y instance Foo Int Bool we are positive there may not be any instance 'Foo Int <anything>' ever again, open world and -fallow-overlapping-instances notwithstanding. In fact, it is because we are so positive about that fact that we may conclude that "Foo Int x" implies x = Bool. At least in the case of functional dependencies, the way to close the world gives us type improvement rules. One might wonder if there are other ways to (semi-)close the world with similar nice properties.
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
participants (6)
-
C T McBride -
Frank Atanassow -
hancock＠spamcop.net -
John Meacham -
oleg＠pobox.com -
Simon Peyton-Jones