
Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): return a >>= f ≡ f a I figured out that there is the "distinguishing" context (seq [] True) which falsifies the law for a and f defined below
let a = True let f = \x -> (undefined::IO Bool) seq (return a >>= f) True True seq (f a) True *** Exception: Prelude.undefined
Is there a side-condition of the law I missed? Regards, David

On Tue, Mar 2, 2010 at 1:17 PM, David Sabel
Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad):
return a >>= f ≡ f a
I figured out that there is the "distinguishing" context (seq [] True) which falsifies the law for a and f defined below
let a = True let f = \x -> (undefined::IO Bool) seq (return a >>= f) True True seq (f a) True *** Exception: Prelude.undefined
Is there a side-condition of the law I missed?
No, IO just doesn't obey the laws. However, I believe it does in the seq-free variant of Haskell, which is nicer for reasoning. In fact, this difference is precisely what you have observed: the distinguishing characteristic of seq-free Haskell is that (\x -> undefined) == undefined, whereas in Haskell + seq, (\x -> undefined) is defined. Operationally speaking, GHC cannot normalize an expression with IO without executing the IO, because of the evaluation model. Luke

On 2 March 2010 15:44, Luke Palmer
On Tue, Mar 2, 2010 at 1:17 PM, David Sabel
wrote: Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad):
return a >>= f ≡ f a
I figured out that there is the "distinguishing" context (seq [] True) which falsifies the law for a and f defined below
let a = True let f = \x -> (undefined::IO Bool) seq (return a >>= f) True True seq (f a) True *** Exception: Prelude.undefined
Is there a side-condition of the law I missed?
No, IO just doesn't obey the laws. However, I believe it does in the seq-free variant of Haskell, which is nicer for reasoning. In fact, this difference is precisely what you have observed: the distinguishing characteristic of seq-free Haskell is that (\x -> undefined) == undefined, whereas in Haskell + seq, (\x -> undefined) is defined.
In GHC 6.12.1 both expressions reduce to True, but it doesn't happen in GHC 6.10.4. Any ideas why the behaviour is different? -- Andrés

In GHC 6.12.1 both expressions reduce to True, but it doesn't happen in GHC 6.10.4. Any ideas why the behaviour is different?
Maybe (I'm guessing) GHC 6.12.1 is smart enough to figure out that f a is not needed to evaluate True? In docs it was said that seq states that 'it may be beneficial but details are up to compiler. Regards

Hi, thanks for all the comments. In ghc 6.12.1 the behavior is strange: If f is "defined" in the interpreter via let, then the seq-expression converges GHCi, version 6.12.1: http://www.haskell.org/ghc/ :? for help
let f = \x -> (undefined::IO Bool) seq (f True) True True
but if you build a let-expression then it diverges
let f = \x -> (undefined::IO Bool) in seq (f True) True *** Exception: Prelude.undefined
for the first way: if you use another type, then it diverges:
let f = \x -> (undefined::Bool) seq (f True) True *** Exception: Prelude.undefined
Regards, David Andrés Sicard-Ramírez schrieb:
On 2 March 2010 15:44, Luke Palmer
mailto:lrpalmer@gmail.com> wrote: On Tue, Mar 2, 2010 at 1:17 PM, David Sabel
mailto:sabel@ki.informatik.uni-frankfurt.de> wrote: > Hi, > when checking the first monad law (left unit) for the IO-monad (and also for > the ST monad): > > return a >>= f ≡ f a > > I figured out that there is the "distinguishing" context (seq [] True) which > falsifies the law > for a and f defined below > > >> let a = True >> let f = \x -> (undefined::IO Bool) >> seq (return a >>= f) True > True >> seq (f a) True > *** Exception: Prelude.undefined > > Is there a side-condition of the law I missed? No, IO just doesn't obey the laws. However, I believe it does in the seq-free variant of Haskell, which is nicer for reasoning. In fact, this difference is precisely what you have observed: the distinguishing characteristic of seq-free Haskell is that (\x -> undefined) == undefined, whereas in Haskell + seq, (\x -> undefined) is defined.
In GHC 6.12.1 both expressions reduce to True, but it doesn't happen in GHC 6.10.4. Any ideas why the behaviour is different?
-- Andrés

David Sabel wrote:
when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): I figured out that there is the "distinguishing" context (seq [] True) which falsifies the law...
It's worse than that - Haskell types and functions do not even form a category under Haskell composition: Prelude> seq (id . undefined) 42 42 Prelude> seq undefined 42 *** Exception: Prelude.undefined So (id . undefined) /= undefined, violating one of the category laws. This is not just a problem with IO - it's a problem with Haskell itself. Luke Palmer wrote:
No, IO just doesn't obey the laws. However, I believe it does in the seq-free variant of Haskell, which is nicer for reasoning.
Ignoring the existence of seq does solve both problems. This seems like a messy solution, because seq really *does* exist, and it seems essential. But it's not as bad as it sounds. Even without the built-in seq, you can define seq manually for most common types: class Seq a where seq :: a -> b -> b instance Seq Int where seq 0 x = x seq _ x = x etc. You just wouldn't have seq for function types. There is another way around this problem in which we don't need to ignore seq. Let's define strict composition: f .! g = f `seq` g `seq` f . g This is "true" function composition in the mathematical sense - it doesn't have the extra layer of laziness that Haskell usually imposes. With strict composition, Haskell types and functions do form a category even when we include seq. Unfortunately, IO still does not satisfy the monad laws. But that could easily be fixed by making return strict, so that return undefined == undefined. (Note also that by "monad laws" here I mean the points-free version of the laws, with strict composition. That is the version of the laws we get if take the mathematical monad laws in the category we have just defined and translate them into Haskell monad notation.) Category theorists tend not to like this method of resolving the problem as much. The category we get this way is lacking some important basic properties, so it is harder for them to work with. But I think it better reflects the reality of Haskell, which does in fact include seq. For this reason, I consider it a bug in GHC that return :: IO a is lazy. Regards, Yitz

On Tue, Mar 2, 2010 at 4:37 PM, Yitzchak Gale
For this reason, I consider it a bug in GHC that return :: IO a is lazy.
Wait a minute... return undefined >>= const (return 42) = const (return 42) undefined = return 42 But if return undefined = undefined, then that equals; undefined >>= const (return 42) Which, if IO is allowed to have effects (i.e. if putStrLn "Hello, World" >>= const (return 42) is to be different than return 42), must be undefined. Or does the former not hold in your version of the laws with strict composition? Luke

Hi Luke, I wrote:
For this reason, I consider it a bug in GHC that return :: IO a is lazy.
Luke Palmer wrote:
Wait a minute...
return undefined >>= const (return 42) = const (return 42) undefined = return 42
But if return undefined = undefined, then that equals;
undefined >>= const (return 42)
Hmm, this is true. OK, so let's explicitly restate the monad laws in this context: (>>= f) .! return == f (>>= return) == id (>>= f) .! (>>= g) == (>>= (>>= f) .! g) David's original problem was with the second law, when you apply the function on both sides to undefined. Let's verify the existence of that problem in the current notation: Prelude> seq ((>>= return) (undefined :: IO Bool)) 42 42 Prelude> seq (id (undefined :: IO Bool)) 42 *** Exception: Prelude.undefined To satisfy the second law, we need: (>>= return) undefined == undefined Why is this not working? Apparently, (>>=) is lazy in its first argument. Then, since return is also lazy, GHC never even looks at the first argument. It just stuffs the operation that includes looking at the first argument into the return-thunk. So there are exactly two ways to satisfy the second law: either (>>=) must be strict in its first argument, or return must be strict. I thought the simplest way out of this would be to make return strict. I didn't notice that there is a problem with it. But you have pointed out that I was being too cavalier. So I now amend my GHC bug report to say: (>>=) must be strict in its first argument. Does that sound better to you? Thanks, Yitz
participants (5)
-
Andrés Sicard-Ramírez
-
David Sabel
-
Luke Palmer
-
Maciej Piechotka
-
Yitzchak Gale