Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 25 Jan 2005, at 08:53, Daniel Fischer wrote: Am Montag, 24. Januar 2005 22:59 schrieb Benjamin Franksen: 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. You are wrong in suggesting that an 'action' must necessarily give the same result every time it is called. Your action (printAndReturnChar getChar) :: IO Char is a single, well-defined member of the type IO Char. Its denotation in a particular model will be something like 'read a character from stdin, print it and then return the value'. One can imagine a simplistic (pure haskell) implementation of IO in which a member of IO a is a list of 'SysCalls' together with a 'wiring diagram' which indicates how to connect together the return values of SysCalls. Others have alluded to concrete implementations along these lines but a bit more sophisticated. 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. I think you misunderstand 'pure type IO Char'. Being of 'pure type IO Char' does not mean that you will always return the same Char value. Does it help you to think of the State monad? It is easy to imagine a value of (pure!) type State s Char which returns a different value depending on the state 's' which is passed to evalState. In this way, the return value of an action of type IO Char depends on the state of the real world which is 'passed to it' by the haskell main loop (which is the analogue of evalState for the real world). 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, 1 is quite incorrect. Two values of type 'State s a' can be precisely the same (even syntactically the same, which is stronger) and still return different results when run in different states. 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? The 'relevant' side effects are approximately 'Syscalls'. These include all such things as reading/writing, generating random numbers, opening network sockets, displaying windows, and so on. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Daniel Fischer [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 [EMAIL PROTECTED], Keean Schupke [EMAIL PROTECTED] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 25 Jan 2005, at 10:32, Keean Schupke wrote: I think I see, but if the objects are types, arn't the morphisms functions on types not values? 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. mu is a natural transformation between the functor TT and the functor T. eta is a natural transformation between the identity functor iota and the functor T. A natural transformation is defined as a (natural) family of morphisms, so mu is defined by a family of functions mu_a : T T a - T a That is, for every type 'a' there is an ordinary function mu_a of type T T a - T a. In particular, for a == Int, there is a function mu_Int : T T Int - T Int. For T as the list monad [], mu_Int is concat : [[Int]] - [Int] For T as the IO monad, mu_Int is the function IO IO Int - IO Int given by 'the action which consists of doing all the actions from the outer IO followed by all the actions from the inner IO' Similarly, eta_Int : Int - [Int] is (\x - [x]), eta_IO : Int - IO Int is 'the action which does nothing and then returns x' Then the monad laws (associativity for mu, and left/right unit laws for eta over mu) must hold for all types. At each type, they refer to equality on functions, which is defined pointwise, so they must be equal at all values. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 25 Jan 2005, at 11:49, Keean Schupke wrote: Jules Bean wrote: 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). T is an endofunctor (mapping functions on types to functions on types *and* types to types) : functors map not only morphisms but also objects. 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? I don't know. The reason I don't know, is I can't actually find written down the laws that MonadPlus is 'supposed' to obey. I agree with the OP (ashley, IIRC) that mzero and the IO monad behave in a surprising way. I would think that the closest I could get to a 'sane' definition of MonadPlus for State Monads is something which for mzero goes into a 'special state' representing exception (with undefined for a value, I suppose), and for mplus tries the left branch, if that goes into the exception state then tries the right branch. 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? 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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- Tand 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 25 Jan 2005, at 12:22, Jules Bean wrote: The concrete example for [] is: concat . (map concat) should be the same (on all values of all types [a]) as concat . concat ..tiny correction, sorry. 'On all values of all types [[[a]]]'. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On Tuesday 25 January 2005 02:25, Jan-Willem Maessen wrote: 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 ... return 5 Opss, of course... J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 25 Jan 2005, at 13:20, Keean Schupke wrote: 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. Good paradox. That is what is upsetting me, too. Acutally looking at GHC CVS libraries, there is not a definition for MonadPlus on the state or IO monads... It's in Control.Monad.Error. Not documented though. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 24 Jan 2005, at 18:18, Keean Schupke wrote: 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. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. 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: 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 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
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On Monday 24 January 2005 21:23, Daniel Fischer wrote: 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 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. (unless we index them with the space-time-coordinates of their invocation). No need to do that. 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. If you cannot agree, I have another question: is return 4 return 5 == return 5 true in the IO-Monad? Why, yes of course. That doesn't mean you can generalize it arbitrarily. It is true, because 'return 4' has no effect, other than returning '4' which is ignored by the '' operator. In our operational model, 'return 4 return 5' has exactly the same externally visible effect as 'return 5', so they are equal. From the 'just the result matters'-point of view, obviously. From the 'everything matters'-point of view not. 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. 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), The above equality depends on what sin and cos mean. Regarded as functions on real numbers it is correct. It is false if they are considered functions on floating point numbers (and thus only approximating the 'real' sin/cos). 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. As I said, this is complete nonsense. 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. 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... 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Am Montag, 24. Januar 2005 20:25 schrieb Keean Schupke:
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.
You lost me there.
As I see it, the objects of C are the types, i.e.
Ob(C) = {T : T is a Haskell type}.
I'd say that a type is a set of values, but that doesn't matter really.
The Morphisms of C are the functions between types, i.e.
Mor(A, B) = {f : A - B}.
Then IO is (supposed to be) a functor C - C, that is, to every object A we
have an associated one, namely IO(A), and to every morphism f `elem` Mor(A,B)
we have an associated one, IO(f) `elem` Mor(IO(A), IO(B)).
Further we have a natural transformation, eta, from the identity functor to
IO, that is, for every A `elem` Ob(C) we have an eta_A `elem` Mor(A, IO(A)),
such that
(forall A,B `elem` Ob(C)) (forall f `elem` Mor(A, B))
(eta_B . f == IO(f) . eta_A)
and a natural transformation mu from IO . IO to IO, that is, for every A
`elem` Ob(C) we have a mu_A `elem` Mor(IO(IO(A)), IO(A)), such that
(forall A,B `elem` Ob(C)) (forall f `elem` Mor(A, B))
(mu_B . IO(IO(f)) == IO(f) . mu_A).
Now, eta is return and mu is join, or mu_A = (= id_(IO(A))).
Finally, in order to make the triple (IO, eta, mu) a Monad, eta and mu must
meet three conditions:
i) mu . IO(mu) = mu . mu, or, more clearly
(forall A `elem` Ob(C)) (mu_A . IO(mu_A) == mu_A . mu_(IO(A))),
ii) mu . eta == id, or
(forall A `elem` Ob(C)) (mu_A . eta_(IO(A)) == id_(IO(A))),
iii) mu . IO(eta) == id, or
(forall A `elem` Ob(C)) (mu_A . IO(eta_A) == id_(IO(A))).
Each of these conditions demands the equality of some functions, and all of
these functions are in Mor(A, IO(B)) for appropriate A and B.
So the first question to answer -- and I believe the rest will relatively
easily follow from that answer -- is
What does equality mean in type IO(A)?
Without that, the conditions are meaningless, and IO cannot even be a functor.
And suppose we found an answer, such that indeed IO is a functor. Are then
conditions i)--iii) fulfilled?
Condition ii) demands that
return (putStrLn hi) = id == putStrLn hi.
Let's try it out:
Prelude putStrLn hi
hi
(16 reductions, 30 cells)
Prelude return (putStrLn hi) = id
hi
(22 reductions, 36 cells)
Now obviously they aren't absolutely identical, in return .. = id, we
execute the actions of first wrapping up putStrLn hi in a further IO-layer
and then unwrapping it again. So if we insist that equality of IO-actions
means that exactly the same actions are performed, IO is NOT a Monad.
But I don't suppose such a rigid interpretation was intended and in our
running example, there was additional output generated, which is a visible
difference. But is it so important whether WE see a difference or only the
machine does?
Of course, saying that two IO-actions are equal when they return the same
result (given the same input), is not easily accepted, but output isn't the
perfect criterion either: what if stdout is closed? Is
putStrLn hello mzero == mzero then?
I wish someone called Simon could shed some light on this issue.
Daniel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Am Dienstag, 25. Januar 2005 00:29 schrieb Jorge Adriano Aires: x = getLine = putStrLn 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. A constant c :: a is just morphism(function) c : 0 - a, where 0 is the initial object (empty set). ^ The empty set being an initial object means, for every a there is exactly one morphism from 0 to a. A constant is a function from a one-element-set to a. 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? 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. But that is the problem, what does it mean for two actions to be the same? After all, writing hello to stdout is just a side-effect, like putting 4 on the stack and immediately ignoring it. J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
(Sorry about the recurrent self answers) Maybe (not sure) it is sensible to sapecify return::(a - IO a), as an action with no side effects such that return x === return x iff x === x. return x === return y iff x === y-- this is what I meant to write. But even that is not enough, should be: return x is an action with no side effects and that always returns x The previous specification is be a consequence of this one, and it failed to specify that the returned value was always x. J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
G'day all. Quoting Daniel Fischer [EMAIL PROTECTED]: 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). Not really. One of the ways that IO used to be implemented (still might be on some Haskell systems) was as a term language which was effectively interpreted by the run-time system. You could, in principle, define Eq on such a term language, assuming that there weren't any non-Eq values in subterms. So the question is relevant. If you cannot agree, I have another question: is return 4 return 5 == return 5 true in the IO-Monad? It sure is: return 4 return 5 == return 4 = \x - return 5 (defn of ) == (\x - return 5) 4 (return-bind law) == return 5 Now what was the question again? Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 24 Jan 2005, at 09:36, Keean Schupke wrote: 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. This makes no sense to me at all. putStrLn Hello has type IO (). mzero (could) have type IO (). But they certainly do not denote the same element of IO ()! Monad/MonadPlus laws surely apply to the full monadic type m a, not just the value type a? Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
On 24 Jan 2005, at 10:32, Keean Schupke wrote: 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. This is not true. 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. 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. 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. 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. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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 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? 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) 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? ...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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Ashley Yakeley [EMAIL PROTECTED] 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 \__/ [EMAIL PROTECTED] ^^ http://qrnik.knm.org.pl/~qrczak/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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? Yes. 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? 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 = () And this would be correct too: instance MonadPlus Maybe where mzero = Nothing mplus a b = Nothing instance MonadPlus [] where mzero = [] mplus a b = [] 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
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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) Not really. If the recursive call is something like msum [all_possible_paths], then you are backtracking. The difference is that by using Maybe you'll stop as soon as you succeed, and with list you will find all possible paths. I don't have a small, self-contained, example at hand so I'll use one by Carsten Schultz that I once saw posted in comp.lang.functional. Hope he doesn't mind. http://groups-beta.google.com/group/comp.lang.functional/msg/d7ac1fe1684ef840 -- --- -- knapsack problem module Subset2 where import Control.Monad sss :: MonadPlus m = Int - [Int] - m [Int] sss n [] | n0 = mzero sss n (x:xs) = case compare n x of LT - mzero EQ - return [x] GT - liftM (x:) (sss (n-x) xs) `mplus` sss n xs -- --- sss 40 [3, 8, 9, 13, 14, 15, 17, 19] :: [[Int]] [[3,8,14,15],[3,9,13,15],[8,13,19],[8,15,17],[9,14,17]] sss 40 [3, 8, 9, 13, 14, 15, 17, 19] :: Maybe [Int] Just [3,8,14,15] [*] For instance, I've missed Maybe being an instance of MonadError. You could define your own instance, of course. Yes of course, and I did ;) But I think it should be provided nontheless, and I even find the fact that it isn't is playing a big part in all this confusion. Since there is no MonadError instance for Maybe, we end up using its MonadPlus instance, which just happens to be the same. But it cannot be generalized, for other types. Lets forget about lists, think (Either e). It's usual to move from (Maybe a) to (Either e a) to consider more than one kind of error. But, there is no natural instance of MonadPlus for (Either e a). What would mzero be? Yet, the Maybe like, mplus operation makes perfect sense in (Either e) or any other MonadError, though. You don't need Monoids at all, what you need is the concept of error. Just define it as: skipError x y = catchError x (\_-y) J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
I think it would be helpful if all these classes came with their laws prominently attached in their Haddock documentation or wherever. Agree. 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) snip (mplus a b) = c = mplus (a = c) (b = c) 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. Cheers, J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. Nope, I am. Sorry! I was alternating between monoids and monadplus, and came up with that nonsense. I was obviously thinking about Monoid () and not MonadPlus (). 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). Yeap. You are right again. Sorry for this terrible example, please ignore it. J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Ashley Yakeley wrote: In article [EMAIL PROTECTED], S. Alexander Jacobson [EMAIL PROTECTED] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Ashley Yakeley wrote: In article [EMAIL PROTECTED], Keean Schupke [EMAIL PROTECTED] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
Am Samstag, 22. Januar 2005 21:20 schrieb Keean Schupke: Ashley Yakeley wrote: In article [EMAIL PROTECTED], Keean Schupke [EMAIL PROTECTED] 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. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: what is inverse of mzero and return?
snip 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. snip 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? My humble opinion follows. It's still a Monoid, being boring should be no reason not to include it [*]. By taking advantage of typeclasses, we can easily alternate between more elaborate approaches and dull ones (if we have the dull ones available too). 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. [*] For instance, I've missed Maybe being an instance of MonadError. Greetings, J.A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
