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]
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]
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]
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]
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]
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]
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]
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]
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]
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. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
