October 2001 - Haskell

Haskell 98: Enum class
by Simon Peyton-Jones 25 Oct '01

25 Oct '01

| > i_succ' = succ i' | > -- ghc : 2147483648 | > -- hugs: -2147483648 | -- nhc98: -2147483648 | -- hbc: -2147483648 | | > I think Hugs is wrong. Integer shouldn't wrap. | | (Actually, ghc is `wrong': hbc, hugs and nhc98 match the Report's | specification here: succ = toEnum . (+1) . fromEnum | This is confirmed by the description of the semantics in | section 3.10.) Lies, all lies. The default methods do not constitute a specification; in this case at least, they only approximate the truth. The Report is quite specific about what enumFrom and friends should do for Integer (Section 3.10). Admittedly, that's a funny place to have to look. Maybe I should move that stuff from 3.10 to 6.3.4. The Report is (regrettably) silent about what the Integer instances for succ and pred should be, but they should definitely simply add 1 (resp subtract 1). They should emphatically not use the default methods. I will add something to that effect in 6.3.4. However Section 6.3.4 is silent on the question of what succ and pred do at the end of the range. What is (succ maxInt)? Bizarrely, Appendix D.2 (derived instances of Enum) tells us that that's an error. (Bizarre because this fact belongs in 6.3.4 not in D.2.) In summary, I propose the following (presentational) changes to the Report. 1. Move specification of enumFrom and friends from 3.10 to 6.3.4 2. Specify that for bounded types, (succ maxBound) and (pred minBound) are errors. 3. Specify that succ and pred on numeric types just add/subtract 1 (subject to (2) above. 4. Rewrite D.2 to talk about deriving only, not about Enum in general. 5. In Appendix A, the Enum class defn, add comments to explain that the default methods only work for types whose fromEnum/toEnum range fits inside Int. Would that at least make the present sitation clear. Acknowledging that Enum has warty features. Simon

4 3

RE: rank 2-polymorphism and type checking
by Janis Voigtlaender 25 Oct '01

25 Oct '01

Hello, and thanks for the various answers! Martin Odersky writes: > > Simon, > > You are correct to have doubts. Indeed our system would not handle > this case, as type variables can only be instantiated to monomorophic > types, not to type schemes. The closest you can get to it is to wrap > the instance type in a type constructor. I.e. `t' could be > instantiated to > > T (\c. forall d . (c->d) -> d -> d) > > where T was declared > > newtype T = T (\c. forall d . (c->d) -> d -> d) > > But I guess that does not solve Janis's problem. > I'm not sure whether it would. To make things more complicated, the application I had in mind would not only require a rank-3 type and quantification over a type constructor, but also polymorphic recursion. Hmm, I wanted to use the free theorem of g's type, but rethinking I wonder what this actually *means* in the presence of quantification over type constructors. The whole story got so complicated, because I wanted to use a nested type of the form data D a = ... | forall b . F (b -> a) (D b) If I settle for the less general but still useful data D a = ... | F (a -> a) (D a) then I can do without any extensions :-) Regards, Janis. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

1 0

Haskell 2: Enum Classes
by Ashley Yakeley 25 Oct '01

25 Oct '01

OK, I'm from the school of thought that prefers everything to have a precise meaning, even if it means "multiplying entities". The fact is, in Haskell 98 the 'Enum' class does extensive multiple duty. -- data Type a = Type class Enum a where predMaybe,succMaybe :: a -> Maybe a class (Enum a) => BoundedStartEnum a where nthValueFromStart :: Integer -> a valueNthFromStart :: a -> Integer class (Enum a) => BoundedEndEnum a where nthValueFromEnd :: Integer -> a valueNthFromEnd :: a -> Integer class (BoundedStartEnum a,BoundedEndEnum a) => FiniteEnum a where predWrap,succWrap :: a -> a nValues :: Type a -> Integer class (Enum a) => UnboundedStartEnum a where pred :: a -> a class (Enum a) => UnboundedEndEnum a where succ :: a -> a -- Of course, Float, Double and Rational would not be instances of any of these classes. If you need 'add one', 'subtract one' functions, those go with numeric classes, which many Enum types would not be instances of. For instance, the letter 'q' is the successor of the letter 'p', but that does not mean that "'q' = 'p' + 1" is meaningful. -- Ashley Yakeley, Seattle WA

1 0

RE: Enum class
by Jan-Willem Maessen 24 Oct '01

24 Oct '01

"Simon Peyton-Jones" <simonpj(a)microsoft.com> responds to me (and others): > The Report Section 6.3.4 (about Enum) refers back to Section 3.10 for > semantics for enumFrom etc. There you'll find a specification for > what they mean, including Float and Double. If I can improve the > wording > I'd be glad to do so, but it does look defined to me. I found it after a bit of hunting, and still managed to be confused---probably more by the layers of indirection, though. I think the proposed consolidation of 3.10 into 6.3.4 will prove helpful. Both of my proposals: > | * In the report, give clear and explicit definitions of > | enumFrom... for Float and Double. This could be done right now. > | * Definitions of enumFrom... for Int which deal gracefully with > | overflow might be a nice addition to the report as people get them > | wrong. Seem to fall under this response: > Hmm. If the specification is ok, I'm disinclined to add an > implementation > too -- there's every chance I'll get it wrong too! Which I can fully understand given the ensuing discussion by Malcolm Wallace et. al. about the given code for pred and succ! Nonetheless, I've implemented enumeration subtly wrong in too many different ways myself (and I'm not the only one). In an effort to remedy this (and because I opened my mouth and said "there ought to be an implementation"!), I've thrown together a "how to do it" library: http://www.csg.lcs.mit.edu/~earwig/Enum.lhs It features as many Enum functions as possible for types in the following classes: * Bounded Integral (Int, Word, etc.) --- does the right thing with bounds, avoids negative values so Word ought to work, etc. * Bounded. Must fit inside an Int, toEnum and fromEnum must be defined. * Floating. Does appropriately peculiar things with upper bounds of enumerations. * Num. Assumes an unbounded type. This is the weakest point: - We must give a different fromEnum for Integer and RealFrac - We must assume that we *either* have a total ordering Ord or negative numbers for enumFromThen. - Bounded enumeration requires either Ord or some very clever type-specific function. For example, consider defining Enum (Complex a). The code is tested for various fencepost errors, but may still have missed details of the spec even after multiple re-readings. Feel free to send me comments. -Jan-Willem Maessen Eager Haskell Project jmaessen(a)mit.edu

1 0

Re: rank 2-polymorphism and type checking
by cwitty＠newtonlabs.com 24 Oct '01

24 Oct '01

"Simon Peyton-Jones" <simonpj(a)microsoft.com> writes: > So I'm interested to know: if GHC allowed arbitrarily-ranked types, who > would use them? I can't promise that I would use them, but it would certainly give me warm fuzzy feelings to know that they were there. :-) On the other hand, I believe that you can construct in GHC a type which is isomorphic to any arbitrarily-ranked type (with any combination of existential and universal quantification) by creating new data constructors. If this is true, then I'm reasonably content with that. Carl Witty

1 0

Re: Incoherence
by John Hughes 24 Oct '01

24 Oct '01

John Hughes wrote: > I noticed today that the presence or absence of a type signature can > change the RESULT of an expression in Hugs and GHC nowadays. Here's an > example: > > a = (let x = ?x in > x with ?x = 1) > with ?x = 2 > -- a == 2 > > b = (let x :: (?x :: Integer) => Integer > x = ?x in > x with ?x = 1) > with ?x = 2 > -- b == 1 > > It's the infamous monomorphism restriction at work, again, of course. Now, > what are the proof rules for reasoning about implicit parameters again (:-)? As you observed, the dreaded monomorphism is at work here, and that's where the problem lies, not really with implicit parameters. It has been proposed that implicitly parameterized definitions not be subject to the monomorphism restriction, precisely to avoid the problem you highlight, but this unpleasantly makes the monomorphism restriction even more clumsy. The best solution is to find a good way to eliminate the DMR. --Jeff Turning off the MR for definitions with implicit parameters wouldn't really be a good solution either. Observe that you may WANT the behaviour of the first example! Suppose you want to change the value of an implicit parameter in a subexpression, but nevertheless refer to the enclosing value of the parameter there. It's natural to write let oldx = ?x in (...?x...oldx... with ?x = newx) which does indeed make the enclosing value of ?x available in the body... PROVIDED the MR applies to the definition of oldx! Without the MR, you can't regain this behaviour with any type signature: declaring x to be Integer in the examples above leads to a type error (maybe it shouldn't?). What we need is different binding syntax for monomorphic and polymorphic bindings. Roll on := and = ... John

3 2

RE: rank 2-polymorphism and type checking
by Simon Peyton-Jones 24 Oct '01

24 Oct '01

PS to my earlier message. I am not at all certain that the Odersky/Laufer thing would in fact solve Janis's problem. You want not only a rank-3 type, but also higher-order unification, since you want to instantiate 't' to \c. forall d . (c->d) -> d -> d That may just be too hard. But I'm out of my depth here. Maybe a types expert can help. Simon | -----Original Message----- | From: Simon Peyton-Jones [mailto:simonpj@microsoft.com] | Sent: 24 October 2001 09:08 | To: Janis Voigtlaender; haskell(a)haskell.org | Subject: RE: rank 2-polymorphism and type checking | | | Here's the story | | * GHC understands only rank-2 types; your type is rank 3 | | * The reason for this is that type inference for higher-rank | types is tricky. | GHC just squeezes through the door with rank-2 types by | using a neat | hack, but the hack just doesn't cope with higher ranks at all. | | * GHC 4.08 didn't *check* that the type is rank-2, whereas | ghc 5.02 does. | So all versions of your program will be rejected by GHC now, before | it ever gets to type checking. | | * It's true that your test' *does* typecheck in GHC 4.08, but | it's a coincidence! | Certain very special programs will work even with higher | rank types, but | its jolly hard to explain which, so GHC 5 chucks them all out. | | * Nevertheless your program makes perfect sense. I believe | that the Right | Thing to do is to adopt Odersky/Laufer's idea of "Putting | Type Annotations | To Work" (POPL 96). They show how to typecheck | arbitrarily high rank | type provided there are enough type annotations, and Mark | Shields has | recently explained it all to me. But implementing this | would be real work. | | So I'm interested to know: if GHC allowed arbitrarily-ranked | types, who would use them? | | Simon | | | | | -----Original Message----- | | From: Janis Voigtlaender [mailto:voigt@orchid.inf.tu-dresden.de] | | Sent: 24 October 2001 08:00 | | To: haskell(a)haskell.org | | Subject: Re: rank 2-polymorphism and type checking | | | | | | Iavor S. Diatchki writes: | | | | > > > test :: (forall t . (forall a . t a) -> t b) -> b -> b | | > i am not an expert on this, but isnt this rank 3? | | | | Might be. Does this mean I cannot write it in Haskell? But, with | | | | data T a = C | | | | I can write: | | | | test' :: (forall t . (forall a . t a) -> t b) -> b -> b | test' g x = | | case g C of C -> x | | | | Here, the type checker finds out on its own that t is | | instantiated to T. Still, | | why are the annotations in the following code not enough to | | let it also accept | | the definition of "test" (see my earlier message), | | respectively how can I tell | | it that t should be instantiated to t c = forall d . (c->d) | | -> d -> d ? | | | | test :: (forall t . (forall a . t a) -> t b) -> b -> b | | test g x = (g :: (forall a . (forall d . (a->d) -> | | d -> d)) -> | | (forall e . (b->e) -> e -> e)) | | ((\f y -> y) :: (forall a . (forall d . (a->d) -> | | d -> d))) | | (id :: (b -> b)) | | (x :: b) | | | | | | -- | | Janis Voigtlaender | | http://wwwtcs.inf.tu-dresden.de/~voigt/ | | mailto:voigt@tcs.inf.tu-dresden.de | | | | | | _______________________________________________ | | Haskell mailing list | | Haskell(a)haskell.org http://www.haskell.org/mailman/listinfo/haskell | | | | _______________________________________________ | Haskell mailing list | Haskell(a)haskell.org http://www.haskell.org/mailman/listinfo/haskell |

2 1

RE: rank 2-polymorphism and type checking
by Simon Peyton-Jones 24 Oct '01

24 Oct '01

Here's the story * GHC understands only rank-2 types; your type is rank 3 * The reason for this is that type inference for higher-rank types is tricky. GHC just squeezes through the door with rank-2 types by using a neat hack, but the hack just doesn't cope with higher ranks at all. * GHC 4.08 didn't *check* that the type is rank-2, whereas ghc 5.02 does. So all versions of your program will be rejected by GHC now, before it ever gets to type checking. * It's true that your test' *does* typecheck in GHC 4.08, but it's a coincidence! Certain very special programs will work even with higher rank types, but its jolly hard to explain which, so GHC 5 chucks them all out. * Nevertheless your program makes perfect sense. I believe that the Right Thing to do is to adopt Odersky/Laufer's idea of "Putting Type Annotations To Work" (POPL 96). They show how to typecheck arbitrarily high rank type provided there are enough type annotations, and Mark Shields has recently explained it all to me. But implementing this would be real work. So I'm interested to know: if GHC allowed arbitrarily-ranked types, who would use them? Simon | -----Original Message----- | From: Janis Voigtlaender [mailto:voigt@orchid.inf.tu-dresden.de] | Sent: 24 October 2001 08:00 | To: haskell(a)haskell.org | Subject: Re: rank 2-polymorphism and type checking | | | Iavor S. Diatchki writes: | | > > > test :: (forall t . (forall a . t a) -> t b) -> b -> b | > i am not an expert on this, but isnt this rank 3? | | Might be. Does this mean I cannot write it in Haskell? But, with | | data T a = C | | I can write: | | test' :: (forall t . (forall a . t a) -> t b) -> b -> b | test' g x = case g C of C -> x | | Here, the type checker finds out on its own that t is | instantiated to T. Still, | why are the annotations in the following code not enough to | let it also accept | the definition of "test" (see my earlier message), | respectively how can I tell | it that t should be instantiated to t c = forall d . (c->d) | -> d -> d ? | | test :: (forall t . (forall a . t a) -> t b) -> b -> b | test g x = (g :: (forall a . (forall d . (a->d) -> | d -> d)) -> | (forall e . (b->e) -> e -> e)) | ((\f y -> y) :: (forall a . (forall d . (a->d) -> | d -> d))) | (id :: (b -> b)) | (x :: b) | | | -- | Janis Voigtlaender | http://wwwtcs.inf.tu-dresden.de/~voigt/ | mailto:voigt@tcs.inf.tu-dresden.de | | | _______________________________________________ | Haskell mailing list | Haskell(a)haskell.org http://www.haskell.org/mailman/listinfo/haskell |

3 2

Re: Monomorphism, monomorphism...
by Marcin 'Qrczak' Kowalczyk 24 Oct '01

24 Oct '01

Wed, 24 Oct 2001 10:36:22 +0200, Hannah Schroeter <uk1o(a)rz.uni-karlsruhe.de> pisze: > Why not create a dictionary record while compiling the associated > instance (which may, by the H'98 definition, occur only once in > the program)? Instances with contexts are commonly represented as functions which make dictionaries from other dictionaries. So although the function itself is only one, it may be applied many times to the same argument, and we want to unify results of the application, pretending that there exists only one instance for Eq [[[[Int]]]]. > Yes, of course. It's a similar problem like in Cayenne, where type checking > could take infinite time, too. (And what about current ghc Haskell, > with multiple parameter type classes, overlapping instances, perhaps > even -fallow-undecidable-...?!) The same. module Test where class C a where f :: a instance C a => C a main = print (f :: ()) [qrczak ~]$ ghc -c -fglasgow-exts -fallow-undecidable-instances Test.hs Test.hs:4: Context reduction stack overflow; size = 21 Use -fcontext-stack20 to increase stack size to (e.g.) 20 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `C ()' arising from use of `f' at Test.hs:4 `f at [()]' arising from use of `f' at Test.hs:4 When generalising the type(s) for main -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

1 0

RE: Enum class
by Simon Marlow 24 Oct '01

24 Oct '01

> > i_succ' = succ i' > > -- ghc : 2147483648 > > -- hugs: -2147483648 > -- nhc98: -2147483648 > -- hbc: -2147483648 > > > I think Hugs is wrong. Integer shouldn't wrap. > > (Actually, ghc is `wrong': hbc, hugs and nhc98 match the Report's > specification here: succ = toEnum . (+1) . fromEnum > This is confirmed by the description of the semantics in > section 3.10.) Indeed. But the default definitions of enumFrom & friends also don't make much sense for Integer. With nhc98, which presumably is using the default definitions from the report: Prelude> [2147483647 .. 2147483649] [] according to the report, this should yield an error (section 6.3.4 states that fromEnum should report an error if its argument is out of range). Both behaviours seem less than useful to me. GHC returns [2147483647, 2147483648, 2147483649], which is also wrong. Is there a good reason why toEnum & fromEnum convert to/from Int rather than Integer? Cheers, Simon

1 0