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

[Graham Klyne]

At 16:00 09/08/04 +0100, Simon Peyton-Jones wrote:
>Any thoughts?

Well, a thought, but I'm not sure that it leads anywhere useful.

In the process of learning Haskell, I've vaguely observed to myself that 
features introduced for describing data (i.e. type expressions) seem to 
also be usable in higher form to describe types.  Mostly, the Haskell 
language definition resists such extension, by sticking with a very simple 
notion of kind and type construction (or is that a fundamental restriction 
of Hindley-Milner?).

For example, if I choose the "wrong" parameter ordering for a type 
constructor in a class declaration, I sometimes find the resulting class 
cannot be used in the ways intended --only one possible sequence of partial 
instantiation is possible-- and have found myself wondering if type-level 
lambda abstraction wouldn't be a useful feature to overcome this.

Your suggestion seems to be another feature in the same vein:  extending 
data features to types.  I find myself wondering where this might all 
end.  If types acquire many of the manipulations that are available for 
data values, then might one find that, in turn, cases will be found that 
seem to require similar capabilities for kinds?

Is there any possibility of a theory that will avoid the need to replicate 
features at higher and higher levels?

(This all seems vaguely reminiscent of the theoretical issues that faced 
denotational program semantics --which I don't claim to understand-- until 
Dana Scott's work showed that there was a logical foundation for treating 
functions as values.  [er, did I get that right?].)

#g
--

>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 at haskell.org
>[mailto:haskell-cafe-bounces at 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 at haskell.org
>| http://www.haskell.org/mailman/listinfo/haskell-cafe
>_______________________________________________
>Haskell-Cafe mailing list
>Haskell-Cafe at haskell.org
>http://www.haskell.org/mailman/listinfo/haskell-cafe

------------
Graham Klyne
For email:
http://www.ninebynine.org/#Contact