- Haskell - Haskell.org

Haskell 98 Standard; library Complex
by George Russell 25 Oct '01

25 Oct '01

I sent a report to SPJ on Tuesday complaining about the Haskell 98 definition of asin on Complex. Whatever the outcome of this report, I think the Haskell 98 definitions for Complex need the following documentational change. We should document, not in Haskell code, but in words, what each function is supposed to do, where there might be any doubt. For example, how do you tell from the definition of sqrt in the standard which of the two possible square roots is being chosen: > sqrt 0 = 0 > sqrt z@(x:+y) = u :+ (if y < 0 then -v else v) > where (u,v) = if x < 0 then (v',u') else (u',v') > v' = abs y / (u'*2) > u' = sqrt ((magnitude z + abs x) / 2) (I think I'll leave this as an exercise for the reader 8-) What is needed is a statement saying that sqrt z approximates the squareroot with phase in [0,pi) (or whatever the answer is). The standard should also specify in words which answer to log, asinh, acosh, atanh, asin, acos, atan, is being chosen.

1 0

Re: [ketil@ii.uib.no: Re: Enum class]
by Dylan Thurston 25 Oct '01

25 Oct '01

(I want to trim the headers, but don't know the history of this thread. Also cc:ed back to the Haskell list.) On Thu, Oct 25, 2001 at 11:11:42AM +0200, Ketil Malde wrote: > Dylan Thurston <dpt(a)math.harvard.edu> writes: > > I agree that Enum instances for Float/Double are not likely to be > > useful. > > From a gut feeling, I could see a use for expressions like > > [1.5, 1.6..] and [1.5, 1.6..2.0] > > (i.e. enumFromThen and enumFromThenTo) but enumFrom and enumFromTo > making list of rounded integers seems strange to me. > > It seems to me that enumFromThen and -To could be implemented > something like: > > enumFromThen beg next = beg : enumFromThen next (next+delta) > where delta = next-beg > > similarly for enumFromThenTo, of course. > > i.e. depending only on functionality found in Num. Why not put these > functions there, and remove Float and Double as Enum instances? > > What am I missing? Currently you can write data Day = Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday weekdays = [Monday..Friday] which has nothing to do with Num. Best, Dylan Thurston

1 0

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