Ashley Yakeley wrote:

In article , "S. Alexander Jacobson" wrote:

...

I assume there is a standard name for this class/function:

instance Foo [] where foo [] = mzero foo (x:_) = return x

instance Foo (Maybe x) where foo Nothing = mzero foo Just x = return x

Surely they are incomplete monad definitions (has a return but no bind)...

I don't believe so. I had to write my own classes to do this sort of thing.

This is also a good opporunity to point out an ambiguity in the standard MonadPlus class. All instances satisfy these:

mplus mzero a = a mplus a mzero = a

But only some instances (such as []) satisfy this:

(mplus a b) >>= c = mplus (a >>= c) (b >>= c)

Other instances (IO, Maybe) satisfy this:

mplus (return a) b = return a

I think mplus should be separated into two functions. This code shows the difference a bit more clearly:

do b <- mplus (return True) (return False) if b then mzero else return ()

For the first kind this is the same as "return ()", for the second kind it's the same as "mzero".

But isnt the point of Monad plus, that to have a 'zero' implies failure (a normal monad cannot fail) - and failure implies choice (a `mplus` b) is a if a succeeds or b if a fails and b succeeds,or mzero if both fail. if you look at your first identity: mplus mzero a = a mplus a mzero = a This fits the above description, but I don't see how the following can be true: (mplus a b) >>= c = mplus (a >>= c) (b >>= c) The LHS says (if a fails run b) then run c. The RHS says if (a then c) fails run (b then c) Finally, mplus (return a) b = return a Is obvious because "return a" is not "mzero", so it is true for all Monads that can fail. Or have I missed the point? Keean.

Am Samstag, 22. Januar 2005 10:09 schrieb Ashley Yakeley:

In article <41F211FB.3030706@imperial.ac.uk>,

Keean Schupke wrote:

...

This fits the above description, but I don't see how the following can be true:

(mplus a b) >>= c = mplus (a >>= c) (b >>= c)

Try it (and my test code) with [], which is an instance of MonadPlus. mplus is defined as (++) for [].

Well, mathematically, a MonadPlus m is a functor into the category of monoids. With the appropriate options, we can write instance Monad m => Functor m where fmap = liftM -- so we see that any Monad is a functor (if >>= is properly defined) -- instance MonadPlus m => Monoid (m a) where mempty = mzero mappend = mplus and feed that into ghc or hugs. Only the monoid Maybe a is not very nice (nor is the monoid IO a),since the second argument of the composition is in general ignored. Actually we can make every nonempty set a monoid in this way, choose an element x1 and define the composition (#) by x1 # x = x, y # z = y, if y /= x1. Now the second argument to (>>=) is an arbitrary function into some monoid and there is no reason why (>>= c) should be a morphism in the category of monoids -- for the trivial monoids just defined, it would naturally be simply c itself. It is a nice feature of lists that (>>= c) is a homomorphism there, but that is only so because (>>=) is appropriately defined. However, (>> k) is, if I see it correctly, a monoid-homomorphism in all these cases -- though somewhat boring. So I think, rather than separating mplus, one should think about whether it is sensible to make Maybe and IO instances of MonadPlus in the first place. I don't know nearly enough of the innards of Haskell to form a valuable opinion of that, but perhaps somebody could enlighten me? Regards, Daniel

In article <200501230458.57938.jadrian@mat.uc.pt>, Jorge Adriano Aires wrote:

One common example is using MonadPlus for some backtracking algorithm, then instantiatiating it to Maybe or List instance depending on wether you just want one solution or all of them.

Backtracking only works with the first kind, even if you're only interested in the first solution. This must hold: (mplus a b) >>= c = mplus (a >>= c) (b >>= c) My test code is a backtracking example: do b <- mplus (return True) (return False) if b then mzero else return ()

[*] For instance, I've missed Maybe being an instance of MonadError.

You could define your own instance, of course. -- Ashley Yakeley, Seattle WA

Ashley Yakeley wrote:

In article <41F211FB.3030706@imperial.ac.uk>, Keean Schupke wrote:

...

This fits the above description, but I don't see how the following can be true:

(mplus a b) >>= c = mplus (a >>= c) (b >>= c)

Try it (and my test code) with [], which is an instance of MonadPlus. mplus is defined as (++) for [].

but what if (a >>= c) causes c to fail, and (b >>= c) lets c succeed. In this case the LHS will fail, whereas the RHS will succeed I think? Keean.

Daniel Fischer wrote:

That's probably a misunderstanding due to the notation, in the [] monad, it's

just

concat (map c (a ++ b)) = concat (map c a) ++ concat (Map c b),

which is easily seen to be true (if applying c to an element of a causes an error, neither side will go past that).

Daniel

So do we consider [] to be fail?, Monad.hs defines: instance MonadPlus [] where mzero = [] mplus = (++) What would happen if this was the definition? instance MonadPlus [] where mzero = [] mplus a b | a == [] = b | otherwise = a Keean.

Jorge Adriano Aires wrote:

On the list monad, I think of the mplus operation as the "union" two non-deterministic states. Mzero is the state that works as the identity (which is when you have no possible state at all).

Okay... thats a definition of a monoid.

...

What would happen if this was the definition?

instance MonadPlus [] where mzero = [] mplus a b

| a == [] = b | otherwise = a

Isn't the above a monoid as well?

a `mplus` [] = a [] `mplus` b = b Still looks like an identity to me.... Is there only on correct definition of a monad/monoid on lists - or does anything that satisfies the monad laws count? I got the impression you could define anthing you liked for mzero and mplus - providing the laws are upheld?

Then, I'd say you're not thinking of monadic sums, but of catching errors, and the appropriate place for that is the class MonadError.

I am thinking about how some monads are summed - like Maybe and the Parser monad. It seems there are two possibilities - either the definitions of MonadPlus for Maybe and Parser monads are in Error, or there can be two different acceptable definitions of MonadPlus on the List? Keean

Aaron Denney wrote:

You can, but the "other one" turns it into a copy of the Maybe Monad, so the current one is more useful.

So what does this mean in terms of Ashley's question: But only some instances (such as []) satisfy this: (mplus a b) >>= c = mplus (a >>= c) (b >>= c) Other instances (IO, Maybe) satisfy this: mplus (return a) b = return a Does it mean that both fall within the acceptable definition of the monad laws for MonadPlus? 1. |mzero >>= f == mzero| 2. |m >>= (\x -> mzero) == mzero| 3. |mzero `mplus` m == m| 4. |m `mplus` mzero == m| So I guess I must have missed the point because the distinction between say a monad on [] and Maybe for example seems to me to be irrelevant to MonadPlus. The distinction comes down to mplus being the same as skipError for Maybe and different for []. Keean.

I got the impression you could define anthing you liked for mzero and mplus - providing the laws are upheld?

I agree that a law-based approach is the correct one. The "Monad laws" are well known, equivalent laws for Functor don't seem to be talked about so much but I doubt there'd be any argument about them, given that Functor is supposed to represent a well-defined concept in category theory. These are found in [1]: fmap id = id fmap (a . b) = (fmap a) . (fmap b) I think it would be helpful if all these classes came with their laws prominently attached in their Haddock documentation or wherever. The trouble with MonadPlus is that the precise set of associated laws is either unspecified or not the most useful (I assume there's a paper on the class somewhere). I think everyone can agree on these: mplus mzero a = a mplus a mzero = a mplus (mplus a b) c = mplus a (mplus b c) mzero >>= a = mzero But what about this? a >> mzero = mzero It's satisfied by [] and Maybe, but not IO (for instance, when a is 'putStrLn "Hello"'), but IO has been declared an instance of MonadPlus. And then there are the two I gave: (mplus a b) >>= c = mplus (a >>= c) (b >>= c) ...which is satisfied by [], but not Maybe or IO. mplus (return a) b = return a ...which is satisfied by Maybe and IO, but not [], although your alternative declaration would make [] satisfy this and not the previous one. [1] Mark P. Jones, _Functional Programming with Overloading and Higher-Order Polymorphism_, 1995 -- Ashley Yakeley, Seattle WA

Am Sonntag, 23. Januar 2005 13:21 schrieb Keean Schupke:

Ashley Yakeley wrote:

...

I think it would be helpful if all these classes came with their laws

prominently attached in their Haddock documentation or wherever. The

Definitely!

...

trouble with MonadPlus is that the precise set of associated laws is either unspecified or not the most useful (I assume there's a paper on the class somewhere). I think everyone can agree on these:

mplus mzero a = a mplus a mzero = a mplus (mplus a b) c = mplus a (mplus b c)

I think it would be even better if the classes came with assertions that 'enforced the laws'... I think this requires dependant types though.

...

mzero >>= a = mzero

But what about this?

a >> mzero = mzero

Well it was in the list I saw... I we consider the familar arithmetic product a * b * 0 -- it is clear that an mzero anywhere in a sequence should result in mzero:

a >> b >> mzero >> c >> d = mzero

But that says nothing about the co-product... where mzero should be the identity IE:

a `mplus` mzero = a mzero `mplus` a = a

But I am not sure there are any requirements on commutivity or associativity on the co-product operation?

I'm afraid I don't understand what you mean by that. I know what a product and a coproduct are in any category, but that's obviously something completely different. In what way should one think of (>>) as a product? With lists, I can see a vague analogy, but in the IO-case, I can't, there I read a1 >> a2 as 'first do a1, then a2'. It's an associative law of composition, yes, but takes arguments of different types, and has no identity (lots of left identities, return whatever; but no right identity -- that's also true for lists and Maybe, by the way). So why make an analogy with ordinary multiplication?

...

It's satisfied by [] and Maybe, but not IO (for instance, when a is 'putStrLn "Hello"'), but IO has been declared an instance of MonadPlus.

from an earlier message of Keean:

1. |mzero >>= f == mzero| 2. |m >>= (\x -> mzero) == mzero| 3. |mzero `mplus` m == m| 4. |m `mplus` mzero == m|

What exactly does 2. mean in the IO-case? a) the results of both calculations are equal -- then it also holds for IO. b) both produce the same output and the same result -- then it doesn't hold for IO. I think, a) is the correct interpretation.

...

And then there are the two I gave:

(mplus a b) >>= c = mplus (a >>= c) (b >>= c)

And what about x >>= (\y -> (c y) `mplus` (d y)) == (x >>= c) `mplus` (x >>= d) or, less general x >> (a `mplus` b) == (x >> a) `mplus` (x >> b)? This is satisfied for Maybe and IO, but not for [], where it's only true modulo a permutation. If we pair (>>) with (*) and `mplus` with (+), I find this a very natural law too. The problem is of course that neither (>>) nor `mplus` are commutative, so we shouldn't expect a strong analogy anyway.

This was not on the list I saw - guess it could either be an omission, or it has nothing to do with "MonadPlus" ... monads with identity and co-product?

again, what do you mean by co-product? MonadPlus says simply that on every m a we have a monoid-structure. The laws 1. and 2. above relate one aspect of this structure with the Monad-structure, namely once we hit mzero, we can't get away from it (and it doesn't matter how we got there). Any stronger relation is sheer luck. We can do something pretty ugly with lists. instance MonadPlus [] where mzero = [] [] `mplus` lis = lis lis `mplus` [] = lis l1 `mplus` l2 = take 3 (l1 ++ l2) Now mplus (return 1) [2,3] == [1,2,3]; (mplus [1,2] [3,4]) >> [5,6] == [5,6,5,6,5,6]; ([1,2] >> [5,6]) `mplus` ([3,4] >> [5,6]) == [5,6,5]; [1,2] >> ([3] `mplus` [4]) == [3,4,3,4]; ([1,2] >> [3]) `mplus` ([1,2]>>[4]) == [3,3,4]. So none of the -more or less natural- relations discussed so far holds in this case.

...

...which is satisfied by [], but not Maybe or IO.

mplus (return a) b = return a

...which is satisfied by Maybe and IO, but not [], although your alternative declaration would make [] satisfy this and not the previous one.

But one could make up any arbitrary law that is satisfied by some definition of a Monad and not others. Presumably there has to be some sound category-theoretic reason for including the law?

Keean

Well, one might prescribe any set of rules that should be satisfied by a MonadPlus, then any instance declaration violating one of them would be -what? Bad style at least. But it's the same with Functor or Monad, no way to guarantee the laws. I suppose, if in category theory there was a definition of MonadPlus requiring additional laws, they would have been included in the above list and no offending instances would have been declared. By the way, does anybody know any sources where a non-category-theorist can learn what Monad and MonadPlus are? (Functors, of course, but what sort?) Daniel

Ashley Yakeley wrote:

I disagree. Clearly (putStrLn "Hello" >> mzero) is not the same as mzero.

Yes it is, side effects are quite clearly not counted. The value of (putStrLn "Hello" >> mzero") is mzero. In reference to the idea of splitting MonadPlus, what category would you be operating in, if you have a zero but no co-product operation? Keean.

Just thinking about this, a monad is a Functor plus two natural-tranformations, Unit and Join. Is there an equivalent definition for MonadPlus... I am not sure I understand where MonadPlus comes from? Is it just a Functor and two different definitions of Unit and Join (from those chosen to be in the class Monad?) Keean.

Ashley Yakeley wrote:

I don't believe this represents a good understanding of IO actions as Haskell values. For instance, 'return ()' and 'putStrLn "Hello"' are the same type, but are clearly different actions and so are usually considered to be different values. That the latter prints out text might be better considered not so much a "side effect" as the actual action itself.

You've introduced the concept of "the value of" an IO action, apparently as something separated from "side effects". I don't believe you can properly define this. For instance, what is the "value" of getChar such that it doesn't involve "side effects"?

Right, but we are dealing with the type system here. Remember Haskell monoids are functors on types, not on values ... (ie the base objects the 'category theory' is applied to are the types not the values)... Therefore we only consider the types when considering Monads. As such if you wished to consider the examples you gave distinct, the type system would need to distinguish side effects... this can be done with a linear-aliasing type system, but not Haskell's as far as I know... Maybe you could write such types: {putStrLn "Hello"; mzero} :: IO (PutStrLn "Hello" => ()) ??? But if we look at the type of the Functor: fmap :: (a -> b) -> m a -> m b Where is the IO action? Keean.

Am Montag, 24. Januar 2005 11:47 schrieb Jules Bean: <snip>

Here are the three monad laws as written on the nomaware site:

1. (return x) >>= f == f x 2. m >>= return == m 3. (m >>= f) >>= g == m >>= (\x -> f x >>= g)

Taking rule 1, we do not simply mean that return x >>= f and f x have the same type. (This is obviously true). We require that they are equal as values of the type m a. In the case of IO, this means that they perform the same action before yielding the same result.

We face a severe problem here, not only that IO a is not an instance of Eq, which takes this whole discussion outside the realm of Haskell, on top of that we find the horrible fact that x /= x may be true in the IO Monad, consider x = getLine >>= putStrLn or anything similar -- actually we already have getChar /= getChar and that holds whether we just consider the values returned by an IO action or take the action performed into account. The sad truth is that IO actions in general aren't well defined entities (unless we index them with the space-time-coordinates of their invocation). So I suggest ending the discussion by agreeing that the question whether or not x >> mzero == mzero holds in the IO-Monad is meaningless (at least, it's fruitless). If you cannot agree, I have another question: is return 4 >> return 5 == return 5 true in the IO-Monad? From the 'just the result matters'-point of view, obviously. From the 'everything matters'-point of view not. I feel a little more at home with the former, because it matches the extensional equality of set theory, but I'm not happy with either. For any mathematician, the function \x -> 2*sin x * cos x IS the same function as \x -> sin (2*x) (given the equality of their respective domains -- though, for ghc they aren't, due to rounding errors), so if we transport this extensionality to our problem -- I am aware that is problematical because of the side-effects -- we get putStrLn "hello" >> mzero == mzero.

Example:

return "hello" >>= putStrLn

this does not only have the same type as putStrLn "hello", and return the same value (), but it also carries out exactly the same actions.

But does it really? hugs thinks otherwise: Prelude> putStrLn "hello" hello () (28 reductions, 55 cells) Prelude> return "hello" >>= putStrLn hello () (31 reductions, 56 cells) Prelude> putStrLn "hello" hello () (26 reductions, 50 cells) even the same input does not necessarily lead to exactly the same actions, depending on whether "hello" is already known or not.

If it was simply enough that it have the same type, then it would be 'good enough' if

return "hello" >>= putStrLn

had the same effect as

putStrLn "goodbye"

...which has the same type, and the same return value.

Yes, definitely a point, if only the result matters, we must say putStrLn "hello" == putStrLn "goodbye", which is somewhat counterintuitive. On the other hand, there are many counterintuitive truths around.

Aside: you said a couple of messages ago:

...

Yes it is, side effects are quite clearly not counted. The value of (putStrLn "Hello" >> mzero") is mzero.

This concept of 'value' only makes sense in some monads. In the List monad there can be many 'values' of a computation. It just happens that IO 'returns' a 'single value' all the time.

Just thinking about this, a monad is a Functor plus two natural-tranformations, Unit and Join. Is there an equivalent definition for MonadPlus... I am not sure I understand where MonadPlus comes from? Is it just a Functor and two different definitions of Unit and Join (from those chosen to be in the class Monad?)

Keean. And these two transformations must satisfy certain conditions. As for MonadPlus, it's just a Monad m with the additional property that forall objects a, the object m(a) is a monoid -- if I'm not mistaken, it also defines a Functor into the category of monoids in our three cases and should do anyway (that's something different from the fact that the object m(a) is a monoid, additionally we must have that for all maps f: a -> b, the associated map fmap f (which should be liftM f) is a monoid-homomorphism; however if we view m as a functor into category Mon, it is no longer a Monad, because then even the concept of a natural transformation of Id to m isn't defined, since

Yes, and return "hello" returns the value "hello", so the concept of value absolutely makes sense in the IO-Monad -- though I would prefer to call "hello" the 'result' of the IO-action, rather than the 'value'. And the result of x >> mzero is mzero, regardless of what x is. Keean: these are functors to different categories). I haven't yet figured out, why exactly mzero >> x and x >> mzero must always yield mzero, that is, the exact interplay between 'bind' and 'fmap', but in our three cases it's natural enough (pace Ashley, Jules and everybody else: if we take the 'results only'-point of view). Aside:

In reference to the idea of splitting MonadPlus, what category would you be operating in, if you have a zero but no co-product operation? ^^^^^^^^^^^^^^^^^^^^^^ I ask again: what is a co-product operation? Can't be the operation of forming the coproduct of a family of objects in a category, sounds like some sort of operation on an object (that would usually be a map ob -> ob -> ob), but I don't know the term, so could someone please explain?

Ashley:

If you remember your category theory, you'll recall that two morphisms are not necessarily the same just because they're between the same two objects. For instance, the objects may be sets, and the morphisms may be functions between sets: morphisms from A to B are the same only if they map each element in A to the same element in B.

Yes, and if your set theory is (for example) NBG without atoms, every object (being an element of a class) is a set, in particular this holds for IO a, so then the question of whether or not putStrLn "hello" >> mzero == mzero hasn't anything to do with functors or category theory, it's just part of the question 'when do you call two elements of IO a equal?' Categories and Monads enter the picture only when we progress to the next question: 'is x >> mzero == mzero necessarily true for all x?' The answer to the second question of course depends on the answer to the first. If category theory says the answer to the second is yes for any Monad(Plus), but we have putStrLn "hello" >> mzero /= mzero, well, then IO isn't a Monad(Plus). However it'd still be useful to pretend it were, I suppose. But I'm still unsure about the first question. And I spend too much time thinking about it. Daniel

Am Montag, 24. Januar 2005 22:59 schrieb Benjamin Franksen:

Both are wrong. 'just the result matters' is the correct POV for functions, but not for IO actions. 'everything matters' is wrong even for IO actions, because the actual value returned when the action is executed is completely irrelevant to the IO action's identity.

Now that I cannot swallow, that would mean return 4 == return 5. I suppose you didn't mean that, though. Maybe, the internal workings are irrelevant, only visible side-effects and the returned value? But which side-effects are relevant?

And also some of the electrons on transistor 19348587434 on the CPU chip move with a slightly reduced velocity due to the computer user shouting curses at his machine...

could that alter the number of reductions?

Seriously, the model in which the 'sameness' resp. identity of IO actions is defined takes into account only (a subset of all) externally observable effects, not the way a certain interpreter/compiler executes the action internally.

I'll stop here; think I have made my point

Yes, and I still don't know which effects do count and why these and not others.

Ben _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Am Montag, 24. Januar 2005 22:59 schrieb Benjamin Franksen:
> I wonder how you derive at this strange conclusion. Of course, getChar ==
> getChar is always true. Now we clearly have to say what we mean by this
> kind of equality. Well, there is an operational model of the program inside
> its environment (OS, etc..) in identity resp. equality of IO actions are
> defined with respect to this model. For instance:
>
> getChar = 'the action that, when executed, reads a character from stdin and
> returns it'
>
> > and that holds whether we just consider the values returned by an IO
> > action or take the action performed into account.
> > The sad truth is that IO actions in general aren't well defined entities
>
> I think the above definition is quite well defined.

I still say, getChar is not a well defined value of IO Char.
If it were, applying a function to it would always produce the same result.
Take the function
printAndReturnChar :: IO Char -> IO Char
printAndReturnChar ioC = do c <- ioC
                                              print c
                                              return c

that produces different results every time a different character is handed to 
getChar. And in this formulation, I see a solution to all this confusion, 
for, as I see it now, getChar is not a value of IO Char at all, it is a 
function with an implicit parameter, its type is actually
getChar :: (?x :: RealWorld) => IO Char.
As such it is of course well defined.
If I'm wrong, please tell me in what way.

> > So I suggest ending the discussion by agreeing that the question whether
> > or not
> > x >> mzero == mzero
> > holds in the IO-Monad is meaningless (at least, it's fruitless).
>
> It is obviously plain wrong.

It is, if the above view is correct, however if you insist on getChar being of 
pure type IO Char, I still have a problem.

> Both are wrong. 'just the result matters' is the correct POV for functions,
> but not for IO actions. 'everything matters' is wrong even for IO actions,
> because the actual value returned when the action is executed is completely
> irrelevant to the IO action's identity.
>
> Seriously, the model in which the 'sameness' resp. identity of IO actions
> is defined takes into account only (a subset of all) externally observable
> effects, not the way a certain interpreter/compiler executes the action
> internally.
>
> I'll stop here; think I have made my point
>
> Ben
Now, I'd say two values of type IO a are the same if (on execution)
1. they return the same result,
2. they have the same relevant side effects.

I think, 1. should be acceptable to everybody, and 2. as a principle too, only 
the question of which effects are relevant needs to be answered. It's plain 
that not all measurable effects are relevant. My inclination to ignore the 
side-effects stemmed from the (irrational) desire to have IO's MonadPlus 
instance justified, now I'm prepared to say yes, side-effects such as output 
do count, so the instance MonadPlus IO is erroneous, but may be maintained 
for practical reasons.

Is there an authoritative list of which side-effects are relevant?
This would settle the question.

Daniel

Daniel Fischer writes:

...

getChar = 'the action that, when executed, reads a character from stdin and returns it'

I still say, getChar is not a well defined value of IO Char.

By this line of reasoning, I think any imperative, real-world interacting program is ill-defined. While in principle, I'd be happy to champion pure functional programs, I would worry that this definition is slighly too narrow to be useful. :-)

If it were, applying a function to it would always produce the same result. Take the function printAndReturnChar :: IO Char -> IO Char printAndReturnChar ioC = do c <- ioC print c return c

This is an IO action parametrized by another IO action.

that produces different results every time a different character is handed to getChar.

But the IO action it returns is still equal to itself, even if it gives different results for different inputs.

And in this formulation, I see a solution to all this confusion, for, as I see it now, getChar is not a value of IO Char at all, it is a function with an implicit parameter, its type is actually getChar :: (?x :: RealWorld) => IO Char.

Or rather: getChar :: (?x :: RealWorld) -> (Char,RealWorld) Which is the whole point of IO, no? So yes, that's the essence.

if you insist on getChar being of pure type IO Char, I still have a problem.

Not if "pure type IO" means RealWorld -> (_,RealWorld)

Now, I'd say two values of type IO a are the same if (on execution) 1. they return the same result, 2. they have the same relevant side effects.

I think, 1. should be acceptable to everybody, and 2. as a principle too, only the question of which effects are relevant needs to be answered.

Well, why not use the same definition as for functions - quoted previously in this thread. They must have the same domain and range, and for each value in the domain, they must give the same result. So for (f,g :: IO a), for these to be equal, they must produce the same value of type a if the state of the RealWorld is equal. "Relevance" isn't necessary for this definition, but I guess you could consider a dimension of the domain irrelevant if the resulting values of f and g is independent of it.

It's plain that not all measurable effects are relevant.

I'm not sure. If I can tell the difference from within my program, I would say that they were different -- even if the difference was "irrelevant" (e.g. one function taking more time than another). But as Eq isn't defined for IO actions, it's a metaphysical question; you can happily call two IO actions the same, even if you can measure a different number of reductions or whatever - for getChar you usually care about input and output, and not about pedantic resource use, so this is not "relevant" in that particular case. (In a real-time setting, you would perhaps ha different criteria for relevance.) Just my opinion, anyway. -kzm -- If I haven't seen further, it is by standing in the footprints of giants

Daniel Fischer wrote:

I think, 1. should be acceptable to everybody, and 2. as a principle too, only the question of which effects are relevant needs to be answered. It's plain that not all measurable effects are relevant. My inclination to ignore the side-effects stemmed from the (irrational) desire to have IO's MonadPlus instance justified, now I'm prepared to say yes, side-effects such as output do count, so the instance MonadPlus IO is erroneous, but may be maintained for practical reasons.

I am sure monads in Haskell (and other functional languages like ML) are defined on types not values. Therefore it only matters that the types are correct and that the operator obeys the associative laws. I am reasonably sure the values whether returned or side-effects are irrelevent. Keean.

I think I see, but if the objects are types, arn't the morphisms functions on types not values? Keean. Ashley Yakeley wrote:

In article <41F61A0B.90005@imperial.ac.uk>, Keean Schupke wrote:

...

I am sure monads in Haskell (and other functional languages like ML) are defined on types not values.

The objects of the category are types. The morphisms on the category are functions. Two functions are the same if they match each value to the same value. For the Functor laws and the Monad laws, the values certainly do matter: if they didn't, they wouldn't correspond to the category theory notions of functor and monad because the morphisms would be wrong.

Jules Bean wrote:

No. Well: they are functions 'on' types, but functions 'on' types map values to values.

Analogy: In the category of sets and functions, the objects are sets and the morphisms are functions. The functions --- from sets to sets --- take objects in one set to objects in another set.

Specifically:

A monad T is a (endo)functor T : * -> * where * is the category of types, together with a multiplication mu and a unit eta.

So, * is the category of Types, and functions on type (which map values to values), and T is an endofunctor (mapping functions on type to functions on type). How does this affect the IO monad though? m >>= (\a -> mzero) === mzero If we consider the state monad, surely the above makes no comment on what the final state should be, only the final value returned... Or is MonadPlus not definable on State monads? If it is then considering IO === ST RealWorld, would imply that the actions of the IO monad are not important as long as the final value returned is mzero? Keean.

Jules Bean wrote:

Well, mzero isn't a return value in the IO monad, it's an exception. But yes, I agree with you that the (plausible) laws I have seen for MonadPlus seem to say that mzero should ignore the actions. But this in practice is not how IO behaves.

Jules

I can see three possible solutions: 1) IO is not an instance of MonadPlus (but may still be an instance of MonadError) 2) Side effects are ignored (or state is ignored) and IO may be an instance of MonadPlus 3) bind (>>=) is redefined for IO. As the IO Monad is a function which resturns a computation, bindIO can be changed such that (a >> mzero === mzero). In other words if the RHS is mzero, the LHS is not included in the final result (and its actions would not get executed), however this must be inconsistent if we consider: f = getChar >>= (\a -> if a == "F" then mzero else return a) In this case if the LHS returns "F" the LHS should not have been run... this contradicts itself, so this is a non option I guess. Acutally looking at GHC CVS libraries, there is not a definition for MonadPlus on the state or IO monads... Keean.

Jules Bean wrote:

It's in Control.Monad.Error. Not documented though.

Jules

Ahh, so it is: instance MonadPlus IO where mzero = ioError (userError "mzero") m `mplus` n = m `catch` \_ -> n So, the author of this obviously subscribed to the view that side-effects are not counted when considering function identity... Keean

In article <41F62049.4010403@imperial.ac.uk>, Keean Schupke wrote:

I think I see, but if the objects are types, arn't the morphisms functions on types not values?

Every morphism in any category has a "from" object and a "to" object: it is a morphism from object to object. In the "Haskell category", a function of type 'A -> B' is a morphism from object (type) A to object B. But in category theory, just because two morphisms are both from object A to object B does not mean that they are the same morphism. And so it is for the Haskell category: two functions may both have type 'A -> B' without being the same function. -- Ashley Yakeley, Seattle WA

On 25 Jan 2005, at 11:56, Keean Schupke wrote:

I guess I am trying to understand how the Monad laws are derived from category theory... I can only find referneces to associativity being required.

Associativity and left and right unit laws.

Monads are defined on functors, so the associativity just requires the associativity of the 'product' operation on functors...

I guess I don't quite see how associativity of functors (of the category of functions on types) implies identity on values... surely just the identity on those functors is required?

The 'associativity' isn't actually saying that the functors are associative. (Functorial composition is of course associativity, that's a fundamental fact about category theory). The 'associativity' is saying that the 'operation' given by the 'multiplication' transformation mu is 'associative'. The proliferation of scare quotes is because monad are not monoids. They are a slightly different notion, but the analogy with monoids is strong, and the words used (multiplication, left and right units, associativity) are borrowed from the words used to talk about monoids. The associativity law says that, given mu : T T -> T (a natural transformation), there are two possible ways of going from T T T -> T using mu, as in (T T) T -mu-> T T -mu-> T and T (T T) -mu-> T T -mu-> T. We require that these two ways be equal as natural transformations. A natural transformation is a natural family of morphisms, and for two natural transformations to be equal, each morphism must be equal. A morphism in this case is a haskell function, and for two morphisms to be equal they must agree on every value. The concrete example for [] is: concat . (map concat) should be the same (on all values of all types [a]) as concat . concat If it helps, the unit laws are that these two functions: Prelude> :t (\x -> concat [x]) (\x -> concat [x]) :: forall a. [a] -> [a] Prelude> :t concat . (\x -> [x]) concat . (\x -> [x]) :: forall a. [a] -> [a] Are both equal (pointwise) to id : [a] -> [a] Jules

We face a severe problem here, not only that IO a is not an instance of Eq, which takes this whole discussion outside the realm of Haskell, on top of

that we find the horrible fact that x /= x may be true in the IO Monad, consider

x = getLine >>= putStrLn

or anything similar -- actually we already have getChar /= getChar

This isn't obvious to me. So x is an action, and it does not always produces the same side effects when executed. But why should that make x/=x? It is the same action, it gets one line from the input, and then prints it... In fact, I do not agree. See Rant 2 below.

The sad truth is that IO actions in general aren't well defined entities (unless we index them with the space-time-coordinates of their invocation). So I suggest ending the discussion by agreeing that the question whether or not x >> mzero == mzero holds in the IO-Monad is meaningless (at least, it's fruitless). If you cannot agree, I have another question: is

return 4 >> return 5 == return 5

true in the IO-Monad?

Yeap, I thought about it too, have no idea, and cannot afford to spend much time thinking about it now either, since I got work to do... :-/ --- Rant 1 My gut feeling would be no. I think my intuitive reasoning is too just consider that, every IO action is equal to itself, then take the closure with respect to function application, and assume all others cannot be proved. That is, x === x, for all x :: IO a f x === g x, for all x :: a and f,g :: a -> IO b, such that f === g Where equality between functions is defined the usual way. --- Rant 2 Nope, we have to have getChar === getChar. I think you'll agree if I say that we have: 1. return === return 2- return 5 === return 5 return 5 >> return 5 === return 5 >> return 5 Because this has nothing to do with IO. 1. We have that, return :: a->IO a is a function, not an action, so it must be equal to itself. 2. We have that, return :: a->IO a is a function, not an action, so it must return the same value when applied to the same element. 3. (>>) :: (Monad m) => m a -> m b -> m b It is also a function, so (>>) x === (>>) x. And by the same reasoning (>>) x y === (>>) x y. So from 2 we have 3. A constant c :: a is just morphism(function) c : 0 -> a, where 0 is the initial object (empty set). So we must have c === c. Which means getChar === getChar. In other words, by questioning wether you can have x ==/= x for x :: IO a, you are questioning wether we really have f === f for all functions f::a->b. ---

...

return "hello" >>= putStrLn

this does not only have the same type as putStrLn "hello", and return the same value (), but it also carries out exactly the same actions.

But does it really? hugs thinks otherwise: Prelude> putStrLn "hello" hello () (28 reductions, 55 cells) Prelude> return "hello" >>= putStrLn hello () (31 reductions, 56 cells) Prelude> putStrLn "hello" hello () (26 reductions, 50 cells)

even the same input does not necessarily lead to exactly the same actions, depending on whether "hello" is already known or not.

This I don't agree with, I think you are using the word actions for two different things, the elements of type IO a, and their execution. What you just showed is that those IO () elements (actions) when executed, always created different side effects in the real world. Not that the actions themselves are different. J.A.

...

This isn't obvious to me. So x is an action, and it does not always produces the same side effects when executed. But why should that make x/=x? It is the same action, it gets one line from the input, and then prints it...

OK, but then the different side-effects could not be used to distinguish putStrLn "hello" >> mzero and mzero. So I still believe, if you say these two are different, because they produce different output, you cannot easily insist on x === x.

Agree. But I don't say that.

...

This I don't agree with, I think you are using the word actions for two different things, the elements of type IO a, and their execution. What you

You're right, but one of my problems is to identify elements of type IO a. If the returned value isn't the thing, the execution must matter, but which parts of the execution are to be taken into account?

How can we tell if functions f === g? They must have the same domain, codomain and return the same result for every element of the domain. This is just the mathematical definition. For any two arbitrary functions f,g, can you tell if they are the same or not? As a definition, I'd be happy to have, x,y :: IO a are the same if, given the same, real world, they produce the same effects and return the same result. Now I'm not saying we can derive that x === x, for x ::IO, from that, but it is certainly consistent with that point of view, so we can take it as an axiom. Which I think we already do. We also have that if f === g than f x === g x. That includes functions of type f,g :: a -> IO b. All seems consistent. Any other "equality" relation should include that one. Is it enough? It's enough to be able to tell that: putStrLn "hello" >> return 3 === putStrLn ("he"++"llo") >>=\ _ return (1+2) And it would say nothing about things like: return 4 >> return 5 ==?== return 5 I can live with it. To prove that two functions are in deed the same, we may use, say, number theory knowledge, which falls outside the scope of haskell. I find it sensible to do the same with actions. Maybe (not sure) it is sensible to specify return::(a -> IO a), as an action with no side effects such that return x === return x iff x === x. If we add that to our knowledge of IO, along with an appropriate specification for (>>=), then we would have: return 4 >> return 5 === return 5 J.A.

On Jan 24, 2005, at 8:53 PM, Jorge Adriano Aires wrote:

And it would say nothing about things like: return 4 >> return 5 ==?== return 5 I can live with it.

I feel obliged to point out (because the repeated references to the question are driving me up the wall) that this simple equality holds in every monad: return 4 >> return 5 === (definition of >>) return 4 >>= \_ -> return 5 === (monad laws) (\_ -> return 5) 4 === (beta reduction) return 5 We don't need to know anything about the semantics, etc. of any other actions the monad might happen to define. -Jan-Willem Maessen

On 25 Jan 2005, at 09:30, Daniel Fischer wrote:

putStrLn "hello" >>= (\_ -> mzero) === (\_ -> mzero) ()

...no. That last identity holds for 'return ()' but not for 'putStrLn "hello"'. The monad law is a law for 'return' not for arbitrary things. Jules

A constant c :: a is just morphism(function) c : 0 -> a, where 0 is the initial object (empty set).

--- Rant2 "correction" Opss I messed up here. Should be terminal should 1-> a (terminal object/unit set). At least that's how I usually think of constants in haskell 1 is ()... so I think I don't know what is a constant in Haskell... Anyway, stopping now. J.A.

On Mon, Jan 24, 2005 at 09:23:29PM +0100, Daniel Fischer wrote: | We face a severe problem here, not only that IO a is not an instance of Eq, | which takes this whole discussion outside the realm of Haskell, on top of that | we find the horrible fact that x /= x may be true in the IO Monad, consider | | x = getLine >>= putStrLn | | or anything similar -- actually we already have getChar /= getChar | and that holds whether we just consider the values returned by an IO | action or take the action performed into account. Eq is a bit of a red herring: function types don't belong to it either, and yet we can still prove that two functions are equal. IO t is an abstract type, but it can still be thought of as having values (distinct from the values of type t, of course). Suppose we take a concrete IO type (simplified by omitting exceptions):

import Prelude hiding (IO, putChar, getChar) import qualified Prelude import Control.Monad

type IO = Resumption SysCall

data Resumption f a = Return a | Resume (f (Resumption f a))

data SysCall a = GetChar (Char -> a) | PutChar Char a

This encodes the idea that an IO computation either returns a value or some instruction to the system, with a continuation to be entered after the corresponding operation has been run. We can define a monad instance for this type:

instance Functor f => Monad (Resumption f) where return = Return Return v >>= f = f v Resume c >>= f = Resume (fmap (>>= f) c)

instance Functor SysCall where fmap f (GetChar k) = GetChar (f . k) fmap f (PutChar c a) = PutChar c (f a)

and we can define the familiar operations:

getChar :: IO Char getChar = Resume (GetChar Return)

putChar :: Char -> IO () putChar c = Resume (PutChar c (Return ()))

and you can write programs as before, except that now they construct values of the concrete IO type. Because the type is concrete, you can say whether or not two values of type IO t are equal (even though it's not in Eq either). But how do you do anything with values of the made-up IO type? With the built-in IO type, we say the external system grabs the result of main and does something mysterious with it. We can do that with this type too, except that the first part of the execution of the action is to transform the concrete type into the built-in IO type:

toIO :: IO a -> Prelude.IO a toIO (Return a) = return a toIO (Resume c) = doSysCall c >>= toIO

doSysCall :: SysCall a -> Prelude.IO a doSysCall (GetChar k) = do c <- Prelude.getChar return (k c) doSysCall (PutChar c m) = do Prelude.putChar c return m

Now one can prove that toIO is a monad transformation that preserves the primitives (ignoring some pesky liftings of types): toIO (return x) = return x toIO (a >>= f) = toIO a >>= (toIO . f) toIO getChar = Prelude.getChar toIO (putChar c) = Prelude.putChar c For example, here's the proof for getChar: toIO getChar = { definition of getChar } toIO (Resume (GetChar Return)) = { definition of toIO } doSysCall (GetChar Return) >>= toIO = { definition of doSysCall } (Prelude.getChar >>= \c -> return (Return c)) >>= toIO = { monad associativity law } Prelude.getChar >>= (\c -> return (Return c) >>= toIO) = { monad left identity law } Prelude.getChar >>= \c -> toIO (Return c) = { definition of toIO } Prelude.getChar >>= \c -> return c = { monad right identity law } Prelude.getChar so we can push toIO all the way down the program we wrote, and any equation we can prove between values of the concrete type becomes an equation between values of the built-in one. There may be other equations one could postulate for the abstract type, but they require operational reasoning about the effect of operations on the system -- they're external to Haskell. To talk about mzero and mplus, we'd need to extend the concrete IO type with exceptions, but that's not too hard.

Ashley Yakeley wrote:

If you remember your category theory, you'll recall that two morphisms are not necessarily the same just because they're between the same two objects. For instance, the objects may be sets, and the morphisms may be functions between sets: morphisms from A to B are the same only if they map each element in A to the same element in B.

Yes, but I though the 'objects' in this case are endofunctors from a type to itself... the the morphisms operate on these endofunctors, the morphisms are unit and join.... such that joining 'unit' to the endofuntor retults in the endofunctor. But I think that as the endofunctor is from the type to itself, the value does not come into it. A -> A `join` unit => A -> A Keean.

Jules Bean wrote:

I've lost track of what you mean by 'this case' and indeed of what you mean by 'join' (did you mean mplus? the word join is normally used for the operation of type m (m a) -> m a, which is not often used directly in haskell)

However, even addressing your point about endofunctors: for two endofunctors to be equal, they must be equal on all objects and all morphisms, which effectively means they must be pointwise equal on all values.

Jules

I think the endofunctors are defined on the types, not the values though. So the object of the category is the endofunctor (Type -> Type), and unit and join are the identity and binary associative operator on which a Monad is defined. return and bind are defined in terms of unit and join. So unit is the identity which when joined to the endofunctor (Type -> Type) results in the same endofunctor... Therefor: (Type -> Type) `join` unit => (Type -> Type) Now as the type of the IO monad is "IO a" we end up with: (IO a -> IO a) `join` unit => (IO a -> IO a) This is true irrespective of any side effects IO may have, as the type is the same for the IO action no matter what side effects it generates. At least thats how I understand it... Keean.

Right, but we are dealing with the type system here. Remember Haskell monoids are functors on types, not on values ... (ie the base objects the 'category theory' is applied to are the types not the values)...

Therefore we only consider the types when considering Monads.

How so? Functors map morphisms and objects from one category into another. class Functor f where fmap :: (a->b) -> f b -> f a We have the two maps there. - The type constructor, maps the objects (types). - The fmap higher order function, maps the morphisms (function between types). Monads are, in particular, functors. So again, the type constructor maps the objects (types) and the mapping on morphisms (functions from one type to the other) is given by liftM (that is, fmap = liftM). Like Ashley Yakeley said, we can have many different functions (morphism) between two types, namely IO a types.

As such if you wished to consider the examples you gave distinct, the type system would need to distinguish side effects...

Why? I don't see how side effects make any difference here... How do you distinguish morphisms f and g: f,g :: Int -> Int f n = 2*n g n = 2+n J.A.

In article <200501231755.45127.jadrian@mat.uc.pt>, Jorge Adriano Aires wrote:

I just checked the paper, "A monadic Interpretation of Tatics", by Andrew Martin and Jeremy Gibbons http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/tactics.pdf

And in deed, these are the listed laws for MonadPlus. On the other hand, Maybe is said to be an instance of MonadPlus.

So now I'm lost.

OK, Martin and Gibbons are to blame, then. I like their list or laws, but they're wrong to say that Maybe satisfies those laws. -- Ashley Yakeley, Seattle WA

Am Sonntag, 23. Januar 2005 15:58 schrieb Jorge Adriano Aires:

I'm not arguing that definition would be "wrong". It is a monoid. This is the instance for ():

instance MonadPlus() where mzero = () mplus a b = ()

Maybe I'm stupid, but: class Monad m => MonadPlus m where mzero :: m a mplus :: m a -> m a -> m a How does () fit into this, () isn't of kind * -> *, as far as I know () Int is meaningless -- just checked, gives Kind Error.

And this would be "correct" too:

instance MonadPlus Maybe where mzero = Nothing mplus a b = Nothing

...

instance MonadPlus [] where mzero = [] mplus a b = []

Both aren't correct, since mzero `mplus` x == x doesn't hold (they're syntactically correct, though).

Which are not really useful. I'm claiming that the fact that Maybe is a trivial Monoid doesn't mean we should "dumb" down other instances, like the one on lists. The usual definition of Monoid on lists is [] as identity and ++ as the monoid operation. That is how it's defined in class monoid, and I expect this relation to hold:

instance MonadPlus m => Monoid (m a) where mempty = mzero mappend = mplus

...

...

Then, I'd say you're not thinking of monadic sums, but of catching errors, and the appropriate place for that is the class MonadError.

I am thinking about how some monads are summed - like Maybe and the Parser monad.

But, this is not how monadic parsers are summed. Just look into the instace of MonadError for Text.ParserCombinators.ReadP.P. Again it would be the case for parsers that would return just one possible parsing, but not for parsers that return [(a,String)].

J.A.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Daniel

But only some instances (such as []) satisfy this:

(mplus a b) >>= c = mplus (a >>= c) (b >>= c)

Other instances (IO, Maybe) satisfy this:

mplus (return a) b = return a

I think mplus should be separated into two functions.

How would we implement the first kind in the Maybe instance of MonadPlus? J.A.

Ashley Yakeley writes:

But only some instances (such as []) satisfy this:

(mplus a b) >>= c = mplus (a >>= c) (b >>= c)

Other instances (IO, Maybe) satisfy this:

mplus (return a) b = return a

I think mplus should be separated into two functions.

This would prevent using mplus in a single parser which - depending on the underlying monad used - backtracks or not. -- __("< Marcin Kowalczyk \__/ qrczak@knm.org.pl ^^ http://qrnik.knm.org.pl/~qrczak/