- Haskell-Cafe - Haskell.org

closed classes [was: Re: exceptions vs. Either]
by Martin Sulzmann 12 Aug '04

12 Aug '04

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 <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.

1 0

Leo editor for literate programing
by Gour 11 Aug '04

11 Aug '04

Hi! I've just stumbled upon Leo outline editor which looks great as a tool for literate programming (see http://webpages.charter.net/edreamleo/front.html) Since lp is a (wide) accepted practice in the Haskell community, I'm wondering whether someone is using it in a daily programming? (however, I've noticed there is no support for Haskell yet, although there are plugins for emacs/vim.) Sincerely, Gour -- Gour | gour(a)mail.inet.hr Registered Linux User | #278493 GPG Public Key | 8C44EDCD

2 3

RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
by MR K P SCHUPKE 10 Aug '04

10 Aug '04

>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!

1 0

RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
by Graham Klyne 10 Aug '04

10 Aug '04

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(a)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(a)haskell.org >| http://www.haskell.org/mailman/listinfo/haskell-cafe >_______________________________________________ >Haskell-Cafe mailing list >Haskell-Cafe(a)haskell.org >http://www.haskell.org/mailman/listinfo/haskell-cafe ------------ Graham Klyne For email: http://www.ninebynine.org/#Contact

2 1

Constructing a 'State Cover' for a FSM
by Stu White 10 Aug '04

10 Aug '04

Hi all I'm trying to construct a cover for a finite state machine and need to devise a strategy beforehand. Thing is I'm having a little trouble. Could anyone suggest a generic strategy that can be used for constructing a cover (things like how I would identify the machines alphabet and so on). Not sure if everyone else calls them covers, so a quick description:- FSM (M) has a finite number of states, so it should be possible to find a finite set of strings (C) which lets you reach each and every state in M from the initial state. ie given any state s you can find a string w = a1a2....am in C for which initial state -> a1.....->am s is a path in M. Any stratagies would be greatly appreciated, thanks Stu --------------------------------- ALL-NEW Yahoo! Messenger - all new features - even more fun!

1 0

RE: [Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
by MR K P SCHUPKE 10 Aug '04

10 Aug '04

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.

1 0

Re: exceptions vs. Either
by MR K P SCHUPKE 09 Aug '04

09 Aug '04

>After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. >end-programmers have to worry much less about handling errors properly. Which is a bad thing! All programmers always have to consider error conditions, if they don't they write buggy code - that's the nature of the beast. I prefer making programmers expicitly face the decisions they are making, rather than have things implicitly handled in a way that hides what is going on from the programmer. Keean.

5 6

Re: [Haskell-cafe] Re: exceptions vs. Either
by MR K P SCHUPKE 07 Aug '04

07 Aug '04

>Sounds like a job for...Type Inference! In Olegs post where he gave examples of how to make exceptions explicit in type signatures: oleg said: > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-undecidable-instances #-} > > module TER where > > class CERROR a c where > darn:: a -> c-> String -> b > > instance Show a => CERROR a c where > darn label _ msg = error $ "Error: " ++ (show label) ++ " " ++ msg > > > data EHead = EHead deriving Show > data ETail = ETail deriving Show > data EJust = EJust deriving Show > > myhead x@([]) = darn EHead x "head of an empty list" > myhead (x:_) = x > > mytail x@([]) = darn ETail x "tail of an empty list" > mytail (_:xs) = xs Now, if we ask GHCi for the type of myhead, we get *TER> :t myhead myhead :: forall a. (CERROR EHead [a]) => [a] -> a ---------------------------------------------------------- As you can see you get the advantage of explicit exceptions, but with type inference. Keean.

1 0

Re: [Haskell-cafe] Type classes... popular for newbies, isn't it?
by Arjun Guha 07 Aug '04

07 Aug '04

I'd rather not do that, but even if I did, the type-variable action would not be reachable in the terminal function. I could specify a functional dependency st -> action (though I've never used it, it would be a fun to learn). I'm curious as to why my class declaration compiles in GHC, as there doesn't seem to be any way to use it. -Arjun On Aug 7, 2004, at 01:06, camarao(a)dcc.ufmg.br wrote: > Hi Arjun. > > How about inserting one more parameter, "action", in your class > definition: > > class (Ord st) => MinimaxState st action where > successors:: st -> [(action,st)] > terminal:: st -> Bool > > instance MinimaxState Int Int where > terminal i = i == 0 > successors i = [(1,i+1), (-1,i-1)] > > Then don't forget to start the compiler/interpreter with > -fglasgow-exts. > > Hope this helps. > > Regards, > > Carlos > >

4 3

Type classes... popular for newbies, isn't it?
by Arjun Guha 07 Aug '04

07 Aug '04

This class definition is giving me a lot of problems with the successor function: class (Ord st) => MinimaxState st where successors:: st -> [(action,st)] terminal:: st -> Bool A trivial example would be: instance MinimaxState Int where terminal i = i == 0 successors i = [(1,i+1), (-1,i-1)] However, I get this error in GHC: Could not deduce (Num action) from the context (MinimaxState Int, Ord Int) arising from the literal `1' at AbTest.hs:7 Probable fix: Add (Num action) to the class or instance method `successors' In the first argument of `negate', namely `1' In the list element: (- 1, (- i) - 1) In the definition of `successors': successors i = [(1, i + 1), (- 1, (- i) - 1)] I have the class definition and the instance definition in seperate files. I don't understand where I'm supposed to put the "probable fix." I don't want it to be in the class definition, since action should be fairly arbitrary. In fact, no matter what I try, I get errors, for example: instance MinimaxState Int where terminal i = i == 0 successors i = [("action",i+1), ("action",i-1)] Cannot unify the type-signature variable `action' with the type `[Char]' Expected type: action Inferred type: [Char] In the list element: ("action", i + 1) In the definition of `successors': successors i = [("action", i + 1), ("action", (- i) - 1)] Any suggestions? -Arjun

3 2