Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
>but if f is exported, that's probably not what you want. Why... Read my post carefully - I am suggesting that you close the class on IMPORT so module X import a import b import c So we close the class here - after reading all possible instances from imported files a,b, and c Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
but if f is exported, that's probably not what you want. And if you give a type sig to f, f:: forall a. C a => a -> Maybe a the type sig will say it's polymorphic, while the improvement rule will say that a must be Int. Simon | -Original Message- | From: André Pang [mailto:[EMAIL PROTECTED] | Sent: 12 August 2004 14:52 | To: Simon Peyton-Jones | Cc: MR K P SCHUPKE; [EMAIL PROTECTED]; [EMAIL PROTECTED] | Subject: Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either] | | On 12/08/2004, at 11:05 PM, Simon Peyton-Jones wrote: | | > module M where | > | > class C a where | >op :: a -> a | > | > instance C Int where | >op x = x+1 | > | > f x = Just (op x) | > | > Under your proposal, I'd infer f :: Int -> Maybe Int, on the grounds | > that C is closed and there is only one instance. | | If I'm reading Keean's posts right, that's exactly his point: if you | only have one instance of class C, then it's valid to improve f's type | to :: Int -> Maybe Int, right? | | If, on the other hand, you had another instance (e.g. instance C Bool), | then the signature of f would have to remain polymorphic. | | | -- | % Andre Pang : trust.in.love.to.save ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
On 12/08/2004, at 11:05 PM, Simon Peyton-Jones wrote: module M where class C a where op :: a -> a instance C Int where op x = x+1 f x = Just (op x) Under your proposal, I'd infer f :: Int -> Maybe Int, on the grounds that C is closed and there is only one instance. If I'm reading Keean's posts right, that's exactly his point: if you only have one instance of class C, then it's valid to improve f's type to :: Int -> Maybe Int, right? If, on the other hand, you had another instance (e.g. instance C Bool), then the signature of f would have to remain polymorphic. -- % Andre Pang : trust.in.love.to.save ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
module M where class C a where op :: a -> a instance C Int where op x = x+1 f x = Just (op x) Under your proposal, I'd infer f :: Int -> Maybe Int, on the grounds that C is closed and there is only one instance. Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of MR | K P SCHUPKE | Sent: 12 August 2004 14:03 | To: [EMAIL PROTECTED]; [EMAIL PROTECTED] | Subject: Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either] | | Okay anybody whish to argue against these points: | | 1) closed or open is the same if no instances overlap | | 2) overlapping instances (open or closed) can break | code in modules which import the defining module | if a new instance is declared in any imported | module. | | 3) code changes in non-imported modules cannot have | any affect on _this_ module. (And here I count | any module in the import tree as imported - at | least in terms of recompilation dependancies) | | The conclusion appears to be it is overlapping instances | that cause code to be 'breakable' by simply defining a new | instance and not closing the class. Closing the class | would appear to have no adverse affects on existing | programs (as it allows better improvement rules) all existing | programs that compile without the better improvement rules | should still compile - just a few more programs will be | valid with the closed assumption? | | Keean. | ___ | Haskell-Cafe mailing list | [EMAIL PROTECTED] | http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
Okay anybody whish to argue against these points: 1) closed or open is the same if no instances overlap 2) overlapping instances (open or closed) can break code in modules which import the defining module if a new instance is declared in any imported module. 3) code changes in non-imported modules cannot have any affect on _this_ module. (And here I count any module in the import tree as imported - at least in terms of recompilation dependancies) The conclusion appears to be it is overlapping instances that cause code to be 'breakable' by simply defining a new instance and not closing the class. Closing the class would appear to have no adverse affects on existing programs (as it allows better improvement rules) all existing programs that compile without the better improvement rules should still compile - just a few more programs will be valid with the closed assumption? Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
W liście z czw, 12-08-2004, godz. 10:30 +0100, Keith Wansbrough napisał:
> If the compiler treated instances as closed in this way, then adding a
> new instance to the program could break existing parts of the program.
> This would be a development nightmare.
Well, this is already possible due to conflicting instances.
It implies a guideline that a library should only add instances for
classes it defines itself, or for types it defines itself. With
multiparameter classes it suffices that at least one of the types
from the instance head is new.
All other cases should be carefully examined to see if the instance is
appropriate, in particular if it's indeed the only "right" instance for
this class/types combination. If that's right, the instances should be
clearly announced in the documentation, and preferably defined in a
separate module to be imported optionally.
This increases the chance that anybody wishing to make a similar
instance will know about that module, and if he still wants to make
a separate instance, then both libraries can be linked together.
This is only a guideline, not a hard requirement.
--
__("< Marcin Kowalczyk
\__/ [EMAIL PROTECTED]
^^ http://qrnik.knm.org.pl/~qrczak/
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
>If the compiler treated instances as closed in this way, then adding a >new instance to the program could break existing parts of the program. But there are many ways to do this... and besides this doesn't really make sense... consider the following: module A defines class X module B imports class X defines some instances module C imports A & B Now, you can add any instance you like to module C and it is never seen by modules A and B... In other words even if you assume closed classes you cannot break an existing module without editing that module or one imported by it (in which case you can break _anything_ by deleting a function) If you don't allow overlapping instances none of this makes any difference anyway - closed or open ... (instance selection cannot change if no instances are allowed to overlap) Finally if you allow overlapping instances you can break existing code (without the closed assumption) just by putting in a more specific instance in a module included in some module using the more general instance. Thoughts? What is the problem with assuming all classes are closed within the available context (imported modules) Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
> Just wondering, but what exacly is the problem with this open/closed stuff? > As far as I understand it new instances can be added to classes in Haskell > (because they are open)... But its not like instances can be added at link > time, and all the instances that you wish to be considered _must_ be > imported into the current module! [..] Sure it's the case that instances are closed in any given build of a program. But they're not closed over the (maintenance / extension) lifetime of that program. If the compiler treated instances as closed in this way, then adding a new instance to the program could break existing parts of the program. This would be a development nightmare. This is just an example of a general principle in language / compiler design - it's not sufficient that the behaviour be specified, it must behave predictably from the programmer's point of view; in particular, local changes shouldn't have global effect. This also comes up in optimisations - you could write a compiler that recognised occurrences of bubble sort and replaced them with quicksort, for example, but it wouldn't be a good idea, because a small change to the code might cause it to no longer recognise it as bubblesort - with a consequent asymptotic slowdown that bears no relation to the change just made. --KW 8-) ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
Just wondering, but what exacly is the problem with this open/closed stuff? As far as I understand it new instances can be added to classes in Haskell (because they are open)... But its not like instances can be added at link time, and all the instances that you wish to be considered _must_ be imported into the current module! That means if we (for example) used two pass compilation we could gather all the instances together first and know that we have all instances for a given class before considering any resolution of overlapping instances. Why is this not done? (personally I don't mind if compilation takes longer if it makes coding easier...) Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
Hi, here's my take on closed classes versus kinds. 1) Closed classes: Consider class Foo x instance Foo Int instance Foo Bool Assume we'd like to prevent that Foo has any other members besides Int and Bool. Haskell follows the open-world assumption. Hence, Foo t is assumed to be true for any type t unless otherwise stated. Oleg suggests to use functional dependency style improvement. Indeed, we'd like to state that "Foo x improves to False for any x different from Int and Bool". The question is how to enforce this condition? I don't think you can by just relying on functional dependencies. 1a) Closed classes in Chameleon: E.g., in Chameleon we can enumerate all cases which should yield False rule Foo Char ==> False rule Foo (a,b) ==> False rule Foo (a->b) ==> False ... But what happens if we define a new type such as data Erk = ...? Well, we'll need to add a new improvement rule rule Foo Erk ==> False 1b) Closed-world assumption: Alternatively, we might want to abandon the open-world assumption and switch to a Prolog-like closed world approach. See section 4.2 in [1] and section 8.1 in [2] for a discussion. Essentially, we impose that Foo x improves to x=Int or x=Bool We can close classes once and for all, however, we're in trouble in case instance declarations are recursive (e.g., Simon's example involves a recursive instance declaration!) Ref: [1] Object-Oriented Style Overloading for Haskell by Mark Shields and Simon Peyton Jones. [2] A Theory of Overloading by Peter J. Stuckey and Martin Sulzmann b) Kinds There's certainly a connection between closed classes and kinds. Assume we have a system that supports closed classes (either by following (1a) or (1b)). Then kind K = T1 | T2 class C (a::K) can be encoded by closed class K x instance K T1 instance K T2 -- T1 and T2 are the only members of K class K a => C a -- C t implies K t which yields failure if t differs from T1 or T2 Martin Oleg wrote: > 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 ' > 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. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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 ' 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. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
>Is there any possibility of a theory that will avoid the need to replicate >features at higher and higher levels? If we consider types, types are a collection of values, for example we could consider Int to be: data Int = One | Two | Three | Four ... Okay, so the values in an integer are connected by functions (operations like plus, multiply) - but we can consider these externally defined (as they are primitives). Also we have special symbols for the values of this type (type constructors are 'values') like 1, 2, 3... etc. Likewise Char is effectively an enumeration of ascii values (or Unicode values). All these standard types behave like enumerations of values. Lists are effectively nested binary products: data List a = Cons a (List a) But I digress, my point is that types are a 'set' of values, and so we can consider the simplest example: data Bool = True | False So bool is a type and True and False are the values 'in' that type - _but_ we can also write: kind Bool = True | False Where Bool is a kind and True and False are values, Kinds are really a different name for "type_of_types"... and this continues upwards forever (a type_of_type_of_types) ... we can effectively flatten this by considering types as values and kinds as types. What is the difference between a type and a value? So we can consider: "data Bool = True | False" to be a relationship between elements at the Nth level (the RHS) and the N+1th level (the LHS). This relationship could be applied at any level, and it should be possible to detemine the level at which we wish to apply this relationship by the context in which it is used. Imagine a function 'not': not :: Bool -> Bool not True = False not False = True we could apply this at the values level: > not True False The type level: class (Bool a,Bool b) => Not a b | a -> b instance True False instance False True How does this differ from the original functional form? can we imagine doing: not' :: Not a b => a -> b but perhaps writing it: not' :: Bool a => a -> not a After all is not 'not' a complete function from Bool to Bool, whatever Bool is? (Bool could be a type or a type of types, or a type of type of types...) Would this not result in greater code re-use? Perhaps classes would become redundant (apart from being used to allow overloading...) My theory here is a bit shakey - but the name Martin Lof springs to mind. Keean. *errata - when I said "Where Bool is a kind and True and False are values" I of course meant w true and false are types! ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
On Mon, 2004-08-09 at 18:05, Graham Klyne wrote: [snip] > 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? As people have bee discussing recently on this list, this is what dependent types gives you. Instead of having a hierarchy of values->types->kinds-> ... where each is classified by the one above it (values by types, types by kinds), dependent types allow you to have types that depend on values in your program. It does indeed allow you to manipulate types using the same manipulations that are available for ordinary data values. The trade off however is that the value system must be decidable (no bottom allowed) or otherwise the type system is undecidable. There are other ways of making the trade off that do allow you use general recursion when you really need to (as Conor posted recently), but then you loose the ability to prove certain things about your programs within the type checking framework and you would have to go back to external proofs. (Of course this is the situation in Haskell anyway, that these kinds of proofs have to be done externally to the program) Duncan ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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â ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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 w
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
kind statements sound like a good idea - a couple of questions spring to mind - what is the parameter of a kind statement (a type or a kind... a kind makes more sense) ... do we have to stop with kinds what about "kinds of kinds" - the statement has identical syntax to a data declaration, is there no way to combine the two, with perhaps a level value? An example of where you may need kinds-of-kinds (etc) is consider peano numbers (declared as a kind) ... now consider we have several implementations (unary - binary etc) which we wish to group together as an equivalent to the Num class. I accept the above is not a good example as this is better served by a class (as you may well want it 'open')... It seems from a theoretical point of view easy to add multiple levels of kinds instead of one level... of course it is probably much more difficault to do this to GHC? Of course with kinds of kinds you either have to annotate the statement with the level - or let the compiler infer the level. The latter seems much more difficault as the same 'level-less-kind statement' could be used on multiple levels... Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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 | [EMAIL PROTECTED] | http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[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 [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
