May 2002 - Haskell - Haskell.org

Re: State monads don't respect the monad laws in Haskell
by S.M.Kahrs 14 May '02

14 May '02

> "S.M.Kahrs" wrote: > [snip] > > I don't think this really solves the problem with the left unit > > (not in general, and not for IO either), > > it merely pushes it to a different place. > [snip] > Not being a category theorist I find this all a bit confusing. Nothing to do with category theory. I took the law you cited and checked it out. > Can you > give an example where with GHC and the fix I suggested you can show that > the associative law has been broken? I didn't try to find a counter example. I tried to prove the result and got stuck: This is the law I was stuck with: m >>= (\x -> k x >>= h) === (m >>= k) >>= h There were two cases to consider, m=R a, and m=M a - the former works out nicely, but with the latter you get: m >>= (\x -> k x >>= h) = M a >>= (\x -> k x >>= h) = M (a >>= \a'->case (\x -> k x >>= h) a' of R b -> return b M c -> c) = M (a >>= \a'->case (k a' >>= h) of R b -> return b M c -> c) and on the other side: (m >>= k) >>= h = (M a >>= k) >>= h = M (a >>= \a'->case k a' of R b -> return b M c -> c) >>= h = M ((a >>= \a'->case k a' of R b -> return b M c -> c) >>= \a''->case h a'' of R b -> return b M c -> c) Assuming that the associativity law holds for the original monad (the one we try to fix for its dodgy left unit) then this can be changed to: M (a >>= \a' -> (\a'->case k a' of R b -> return b M c -> c) a' >>= \a''->case h a'' of R b -> return b M c -> c) = M ((a >>= \a' -> case k a' of R b -> return b M c -> c) >>= \a''->case h a'' of R b -> return b M c -> c) Using associativity again: = M (a >>= \x->(\a' -> case k a' of R b -> return b M c -> c)x>>=(\a''->case h a'' of R b -> return b M c -> c)) = M (a >>= \a' -> (case k a' of R b -> return b M c -> c) >>= \a''->case h a'' of R b -> return b M c -> c) Assuming further that >>= is left-strict we can change that to: = M (a >>= \a' -> (case k a' of R b -> return b >>= \a''->... M c -> c >>= \a''->...)) where the ... is twice the old case h a'' expression. Now, this is the expression why I claimed the left-unit property of the underlying monad would still show: if (return b>>=f) is the same as f b (in the monad we try to fix) then the first part of this case expression simplifies to exactly the same thing as we had derived from the other side of the equation. But if it does not hold, we should be able to construct a counter example using the left-unit counter example from the underlying monad together with, say, k=R. This all under the assumptions that the original monad m satisfied the assoc law and that its >>= is left-strict. Stefan Kahrs

1 0

using error x as a placeholder
by Hal Daume III 14 May '02

14 May '02

I've seen 'error "foo"' or simply 'undefined' used as a placeholder for elements in a structure which we, as programmers, know will be filled in soon. Often this makes the code clearer because the creation of the data structure and filling in its values is separated (you could argue with this, but that's not the point). This troubles me, though, because even though *we* know the elements will be filled in, maybe the strictness analyser doesn't. So, to test this, I wrote the following program: module Main where import Array sumArray :: Array Int Integer -> Integer sumArray arr = sumArray' 0 low where (low,high) = bounds arr sumArray' acc pos | pos > high = acc | otherwise = sumArray' (acc + (arr!pos)) (pos+1) mkArray1 :: Array Int Integer mkArray1 = fillInArr 1 (listArray (1,9999) (repeat undefined)) where fillInArr 5000 arr = arr // [(5000,arr!4999 + arr!5001)] fillInArr 1 arr = fillInArr 2 (arr // [(1,1),(9999,2)]) fillInArr n arr = fillInArr (n+1) (arr // [(n,(arr!(n-1))+(arr!(10001-n))),(10000-n,(arr!(n-1))+(arr!(10001-n))+1)]) mkArray2 :: Array Int Integer mkArray2 = fillInArr 1 (listArray (1,9999) (repeat 0)) where fillInArr 5000 arr = arr // [(5000,arr!4999 + arr!5001)] fillInArr 1 arr = fillInArr 2 (arr // [(1,1),(9999,2)]) fillInArr n arr = fillInArr (n+1) (arr // [(n,(arr!(n-1))+(arr!(10001-n))),(10000-n,(arr!(n-1))+(arr!(10001-n))+1)]) main = print $ (sumArray mkArray1) `mod` 1024 And compiled it using both mkArray1 (which has undefined elements, supposedly) and mkArray2, which doesn't. (I tried to come up with a function with which to fill in the array that was nontrivial, in the sence that it would be difficult to code using accumulators without the explicit recursive 'fillInArr' function.) The timing results were: mkArray1: 11.42u 0.79s 0:13.47 90.6% mkArray2: 24.55u 2.31s 0:30.12 89.1% Which is actually *slower*. Any ideas why? (These were compiled with ghc 5.02.3 -O2 -fvia-c -fall-strict) - Hal -- Hal Daume III "Computer science is no more about computers | hdaume(a)isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume

1 0

Re: State monads don't respect the monad laws in Haskell
by S.M.Kahrs 14 May '02

14 May '02

George Russel wrote: [snip] > I presume it would not in fact be difficult to synthesise a left identity at > the cost of making things slower, thus (forgive any syntax errors, I'm not going to > test this). > > data MonadIO a = Action (IO a) | Return a > instance Monad (MonadIO a) where > return a = Return a > (>>=) (Return a) k = k a > (>>=) (Action act) f = > Action (act >>= (\ a -> case f a of {Return a -> return a;Action act -> act})) Or, more general: data MonadWrap m a = M (m a) | R a instance Monad m => Monad (MonadWrap m) where return = R R x >>= f = f x M x >>= f = M (x >>= \a->case f a of R b -> return b M c -> c) I don't think this really solves the problem with the left unit (not in general, and not for IO either), it merely pushes it to a different place. I think you need the left-unit law for monad m to prove the 'associativity' law for monad (MonadWrap m) The 'associativity' law: m >>= (\x -> k x >>= h) = (m >>= k) >>= h The case in which the situation occurs is m=(M x) with (k x)=(R b). Stefan Kahrs

2 1

Re: State monads don't respect the monad laws in Haskell
by George Russell 14 May '02

14 May '02

Simon Marlow wrote [snip] > So the IO monad in Haskell, at least as we understand it, doesn't > satisfy the monad laws (or, depending on your point of view, seq breaks > the monad laws). [snip] Cheers Simon. One of the awkward things about the Haskell events I implemented is that although I make them an instance of Monad, they don't actually satisfy left identity. Now I can say that "Yes, Event isn't really a Monad, but neither is IO". According to the report > Instances of Monad should satisfy the following laws: > > return a >>= k = k a > m >>= return = m > m >>= (\x -> k x >>= h) = (m >>= k) >>= h so neither IO nor my events satisfy this. Up to now I haven't had any problems with this. Does GHC or any other Haskell compiler actually rely on instances of Monad satisfying left identity? If not, I would suggest dropping the requirement, if it can be done without upsetting category theorists. (What the hell, they stole the term "Monad" from philosophy and changed its meaning, so why shouldn't we?) I presume it would not in fact be difficult to synthesise a left identity at the cost of making things slower, thus (forgive any syntax errors, I'm not going to test this). data MonadIO a = Action (IO a) | Return a instance Monad (MonadIO a) where return a = Return a (>>=) (Return a) k = k a (>>=) (Action act) f = Action (act >>= (\ a -> case f a of {Return a -> return a;Action act -> act})) (I considered doing something similar to turn Events into a real monad, but decided to choose efficiency over category theory. For events its slightly more complicated as you need to handle the choice operator as well.)

2 2

State monads don't respect the monad laws in Haskell
by Simon Marlow 14 May '02

14 May '02

An interesting revelation just occurred to Simon P.J. and myself while wondering about issues to do with exceptions in the IO monad (see discussion on glasgow-haskell-users(a)haskell.org if you're interested). The question we were considering was whether the following should hold in the IO monad: (return () >>= \_ -> undefined) `seq` 42 == undefined as we understand the IO monad it certainly shouldn't be the case. But according to the monad laws: (law) return a >>= k == k a so (return () >>= \_ -> undefined) `seq` 42 => ((\_ -> undefined) ()) `seq` 42 => undefined `seq` 42 => undefined So the IO monad in Haskell, at least as we understand it, doesn't satisfy the monad laws (or, depending on your point of view, seq breaks the monad laws). This discrepancy applies to any state monad. Suppose we define return a = \s -> (s, a) m >>= k = \s -> case m s of (s', a) -> k a s' now return a >>= k => \s -> case (return a) s of (s', a') -> k a' s' => \s -> case (s, a) of (s', a') -> k a' s' => \s -> k a s but (\s -> k a s) /= (k a) in Haskell, because seq can tell the difference. What should the report say about this? Cheers, Simon

3 2

Apparel & Helmet Links - Super sales & Savings
by PlanetMoto.com 14 May '02

14 May '02

1 0

RE: Dependent Types
by Simon Marlow 13 May '02

13 May '02

> I think you're running into a well-known(*) problem with Hugs's > implementation of the monomorphism restriction. > > (*) actually I thought this was a well-known problem, but it doesn't > seem to be mentioned in the Hugs documentation as far as I can see. Here's a bit of background I managed to dig up: http://www.mail-archive.com/haskell@haskell.org/msg05160.html It appears that a change to the monomorphism restriction to match Hugs's behaviour was considered for Haskell 98, but it looks like it never made it into the report (for what reason I'm not sure - the arguments in favour of the change look fairly compelling). Cheers, Simon

1 0

RE: Dependent Types
by Simon Marlow 13 May '02

13 May '02

> However, if I now comment out the functional dependency > > class Encode a b {- | a -> b -} where > encode :: a -> b > > and include the expressions > > x = encode TimeExceeded ExcTTL > > main = putStrLn x > > then Hugs complains > > ERROR "codes.hs" (line 37): Unresolved top-level overloading > *** Binding : x > *** Outstanding context : Encode TimeExceeded > (ICMPCodeTimeExceeded -> b) > > whereas GHC doesn't complain. > > Which is right? I think you're running into a well-known(*) problem with Hugs's implementation of the monomorphism restriction. According to the Haskell report, as long as a restricted binding is used monomorphically in the body of the module, it is ok. In this case, the constraint 'Encode TimeExceeded (ICMPCodeTimeExceeded -> b)' is resolved by the use of 'x' in the declaration for 'main', which forces the type variable b to String. Hugs applies the monomorphism restriction at the binding site, and complains if the binding isn't monomorphic without checking the rest of the module. It also applies defaulting at this point, which means that f = (+42) main = print (f 3 :: Int) also elicits an error in Hugs, but not in GHC. (*) actually I thought this was a well-known problem, but it doesn't seem to be mentioned in the Hugs documentation as far as I can see. Cheers, Simon

1 0

RE: SUGGESTION: haskell-announce mailing list
by Simon Marlow 13 May '02

13 May '02

> yeah, I really like this because oftentimes an announcment > will incite a > discussion, this way people can reply to the announcement on > the haskell > list if they want to discuss it and the people who dont care about > anouncements can just stay on the announce list. > > I Would also be moderately in favor of merging the haskell and > haskell-cafe lists back into one, mainly because I always felt the > distinction was somewhat arbitrary, who knows what > discussions will turn > out to be too long or have interesting tangents until it is > too late and > everyone has said everything on haskell? but this is a > different issue. > I wonder how many addresses are on haskell and not > haskell-cafe or vice There are about 850 people on the haskell list, and about 700 people on haskell-café, and I'm sure that most of the haskell-café members are also haskell members. I'm happy to set up and moderate haskell-announce(a)haskell.org if there's a general consensus that this would be a useful thing. As to whether we should merge haskell and haskell-café - personally I wasn't in favour of the split at the time, but I recall that support was roughly 50/50 in favour. Unless there's an overwhelming majority in favour of a merge I suggest we leave things as they are. Please don't mail the list with "I vote for haskell-announce"-type messages, and direct follow-up discussion to haskell-cafe(a)haskell.org (Reply-to: is set, I hope). Cheers, Simon (with haskell-admin(a)haskell.org hat on)

1 0

�𾴵��Ͽͻ��
by syhua3000 13 May '02

13 May '02

�𾴵��Ͽͻ�� ã� ��(www.9dns.net)Ϊ�˴�л��Լ��ͻ��˾��֧�ֺ��Σ��ٴ��¾ɷ��ܣ��վ�ռ�� ȶ��ȫ��ͬʱ��ǻ��˲�Ʒ�۸��ܸ��ʵķ��񡣣��˾��վ��ȫ�¸İ棺www.9dns.net�� 200M HTML�ռ�+1��۸�150Ԫ/�� 100M�ռ�(֧��ASP)+100M��ҵ�ʾ�+20M ACCESS��ݿ�+1�� 288Ԫ/�� 200M�ռ�(֧��ASP)+200M��ҵ�ʾ�+30M Access��ݿ�+1�� 338Ԫ/�� ֻ��ۼ۸񡣻�ӭѡ��Ҳ��ӭ��Ϊ��ǵĴ��! ��ǻ��и��Żݼ۸�� http://www.9dns.net �� 缼��޹�˾ --------------------------------------------------------------- �е�Ⱥ��ʼ�,��ר��(http://www.21cmm.com) ��CMM��У(http://www.21cmm.com)��Ŀ��ר��

1 0