Tomasz Zielonka wrote:

On Thu, Aug 31, 2006 at 07:23:55PM +0200, Benjamin Franksen wrote:

...

I'd like to know if the following reasoning can be made more precise:

As we all know, the monadic bind operation has type:

bind :: Monad m => m a -> (a -> m b) -> m b

My intuition says that in order to apply the second argument to some non-trivial (i.e. non-bottom) value of type a, the bind operator needs to be able to somehow 'extract' a value (of type a) from the first argument (of type m a).

The bind operator doesn't have to neccesarily apply the second argument to anything. What if m is Maybe, and the first arguments is Nothing?

True, however if the instance for Maybe would have been defined without /ever/ applying the second argument to anything, then wouldn't this necessarily be a trivial monad (however one would need to define 'trivial' here)?

And if the bind operator "wants" to apply the second argument to something, it doesn't have to do it only once - consider the [] monad.

Yes, I should have said: Any non-trivial definition of bind has to apply its second argument at least in _some_ cases and _at least_ once to something non-bottom.

Other examples:

get :: State s s -- from Control.Monad.State

there is no way you can extract an 's' value from "get" alone - you have to supply the state to the whole computation

Cont (const ()) :: Cont () a -- from Control.Monad.Cont

whatever you do, you won't be able to extract an 'a' typed value, non-bottom from this computation. Cont is defined as:

newtype Cont r a = Cont {runCont :: (a -> r) -> r)}

So getting the value out of the monad is not a pure function (extract :: Monad m => m a -> a). I think I stated that, already, in my previous post. I'd even say that the monadic values alone can be completely meaningless. They often have a meaning only relative to some environment, thus are (usually) _effectful_ computations. But we already knew that, didn't we? The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once), and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value. -- And, of course, whether this is actually true in the first place. Would you say that your examples above are counter-examples to this statement (imprecise as it is, unfortunately)? Ben

On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote:

So getting the value out of the monad is not a pure function (extract :: Monad m => m a -> a). I think I stated that, already, in my previous post.

The only generic way of "extracting" values from a monadic value is the bind operator. The lack of extract function is a feature :-) But now I know that you are not really claiming such a function exists.

The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once)

How about using monad laws, specifically: (return x) >>= f == f x We assume that >>= never uses it's second argument, so: (return x) >>= f == (return x) >>= g Combining it with the above monad law we get: f x == (return x) >>= f == (return x) >>= g == g x so f x = g x for arbitrary f and g. Let's substitute return for f and undefined for g: return x = undefined x so return x = undefined Now that seems like a very trivial (and dysfunctional) monad.

and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value.

Not sure what to do with this one. Certainly, for some monads the environment can be empty, eg. for Identity or []. For the IO monad the lack of the "run" function is a feature (Let's pretend that unsafePerformIO doesn't exist - in fact, there is no such function in Haskell 98), but you can say that the RTS runs the "main" IO computation. Informally, it seems obvious that you have to be able to run your monadic computations somehow - otherwise you wouldn't be writing them ;-) I am not sure you can prove it though.

-- And, of course, whether this is actually true in the first place. Would you say that your examples above are counter-examples to this statement (imprecise as it is, unfortunately)?

Well, no, they were counter-examples for the existence of the extract function. As you say, I misunderstood you intent. Best regards Tomasz

Andrea Rossato wrote:

Il Fri, Sep 01, 2006 at 07:22:02AM +0200, Tomasz Zielonka ebbe a scrivere:

...

On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote:

...

So getting the value out of the monad is not a pure function (extract :: Monad m => m a -> a). I think I stated that, already, in my previous post.

The only generic way of "extracting" values from a monadic value is the bind operator. The lack of extract function is a feature :-) But now I know that you are not really claiming such a function exists.

I do not understand this discussion, but I'd like to.

Can you please tell me what you are talking about in terms of this example?

Sure. Your definition of bind (>>=):

newtype M a = TypeConstructor {unpack::(a, String)} deriving (Show)

instance Monad M where return a = (TypeConstructor (a,"")) (>>=) m f = TypeConstructor (a1,b++b1) where (a,b) = unpack m (a1,b1) = unpack (f a)

applies f to something that it has extracted from m, via deconstructor unpack, namely a. Thus, your bind implementation must know how to produce an a from its first argument m. In this case it doesn't even have to use an 'environment', since the value a is really packed together with the monadic value m. In fact for this monad you /do/ have an 'extract' function: extract = fst . unpack However, there are monads like IO for which it is not possible to define such a function (and for IO this is indeed the whole point). However, in order to 'run' (i.e. finally actually use) a monadic value that involves an application of bind, the latter would have to supply some argument to its second argument (which is a function), so there must be some way to 'get an a out of' the first argument m. I struggle to make this 'somehow get an a out of the m' more precise. Cheers Ben

Il Sun, Sep 03, 2006 at 12:26:25AM +0200, Tomasz Zielonka ebbe a scrivere:

On Sat, Sep 02, 2006 at 09:51:26PM +0200, Benjamin Franksen wrote:

...

However, in order to 'run' (i.e. finally actually use) a monadic value that involves an application of bind, the latter would have to supply some argument to its second argument (which is a function),

If I didn't see above, only the following text...

...

so there must be some way to 'get an a out of' the first argument m.

I would answer: Yes, there is a method in Monad which has exactly this purpose: >>=

I tried to describe this stuff in the link below, the best I could. The text is still in part messing but you should be able to understand where I'm headed just from the code... http://www.haskell.org/haskellwiki/Meet_Bob_The_Monadic_Lover andrea

On Sun, Sep 03, 2006 at 01:23:13AM +0200, jerzy.karczmarczuk@info.unicaen.fr wrote:

Tomasz Zielonka:

...

Programmers define the >>= method for their monads because they want to use it to bind computations. They know how to pass result(s) from one computation in their Monad to another, and they put this algorithm in the implementation of >>=. If they didn't care about passing results from one computation to the next one, they wouldn't be using monads in the first place.

Shrug. If these programmers didn't care about passing results from one computation to the next one, they wouldn't use functional programming at all. Hm. Would it still be "programming"?...

I myself wanted to write that then they wouldn't be using a general purpose programming language, but something like HTML, etc. But then I thought that you may want to have "computations" that can't pass values between each other. One example is an algebraic datatype for describing tree-like structures - but you could argue that there is a bottom-up data flow. Anyway, I haven't thought about it too much... Best regards Tomasz

Well, bind is extracting an 'a'. I clearly see a '\ a -> ...'; it getting an 'a' so it can give that to g. Granted, the extraction is very convoluted, but it's there. -- Lennart On Sep 2, 2006, at 19:44 , Udo Stenzel wrote:

Benjamin Franksen wrote:

...

Sure. Your definition of bind (>>=): ... applies f to something that it has extracted from m, via deconstructor unpack, namely a. Thus, your bind implementation must know how to produce an a from its first argument m.

I still have no idea what you're driving at, but could you explain how the CPS monad 'extracts' a value from something that's missing something that's missing a value (if that makes sense at all)?

For reference (newtype constructor elided for clarity):

...

type Cont r a = (a -> r) -> r

...

instance Monad (Cont r) where return a = \k -> k a m >>= g = \k -> m (\a -> g a k)

Udo. -- Streitigkeiten dauerten nie lange, wenn nur eine Seite Unrecht hätte. -- de la Rochefoucauld _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Am Sonntag, 3. September 2006 15:39 schrieb Lennart Augustsson:

Well, bind is extracting an 'a'. I clearly see a '\ a -> ...'; it getting an 'a' so it can give that to g. Granted, the extraction is very convoluted, but it's there.

-- Lennart

But instance Monad (Cont r) where return = flip id (>>=) = (. flip) . (.) -- or would you prefer (>>=) = (.) (flip (.) flip) (.) ? if we write it points-free. No '\a -> ...' around. And, being more serious, I don't think, bind is extracting an 'a' from m. How could it? m does not produce a value of type a, like a (State f) does (if provided with an initial state), nor does it contain values of type a, like [] or Maybe maybe do. And to my eyes it looks rather as though the '\a -> ...' tells us that we do _not_ get an 'a' out of m, it specifies to which function we will eventually apply m, namely 'flip g k'. But I've never really understood the Continuation Monad, so if I'm dead wrong, would you kindly correct me? And if anybody knows a nontrivial but not too advanced example which could help understanding CPS, I'd be glad to hear of it. Cheers, Daniel

On Sep 2, 2006, at 19:44 , Udo Stenzel wrote:

...

Benjamin Franksen wrote:

...

Sure. Your definition of bind (>>=): ... applies f to something that it has extracted from m, via deconstructor unpack, namely a. Thus, your bind implementation must know how to produce an a from its first argument m.

I still have no idea what you're driving at, but could you explain how the CPS monad 'extracts' a value from something that's missing something that's missing a value (if that makes sense at all)?

For reference (newtype constructor elided for clarity):

...

type Cont r a = (a -> r) -> r

instance Monad (Cont r) where return a = \k -> k a m >>= g = \k -> m (\a -> g a k)

Udo. -- Streitigkeiten dauerten nie lange, wenn nur eine Seite Unrecht hätte. -- de la Rochefoucauld _______________________________________________ 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

-- "In My Egotistical Opinion, most people's C programs should be indented six feet downward and covered with dirt." -- Blair P. Houghton

Am Montag, 4. September 2006 07:44 schrieben Sie:

You are right, but I was using "extraction" in a rather non-technical sense. Look at it this way: we have 'x >>= f', let's assume it's the continuation monad. Assuming f has type 'a -> C b' we must have something of type a to be able to call the function be at all. Somehow >>= is able make sure that f is called (modulo non- termination), so I still claim it "extracts" an 'a'. It's not a value that >>= will actually ever get its hands on, it only manages to make sure its passed to f. So somewhere there is an 'a' lurking, or f could not be called.

Perhaps you don't want to call that "extraction", and that's fine by me. :)

-- Lennart

Let me see... (ommitting Cont/runCont for better readability) ma :: (a -> r) -> r f :: a -> (b -> r) -> r start :: b -> r ma >>= f = ma . flip f (ma >>= f) start === ma (flip f start) So we never apply f to a value of type a, we apply it (or rather flip f) to a value of type (b -> r) when we finally run our action to get a value of type (a -> r), which then ma can be applied to. Is that correct? Or what did I get wrong? However, in practice, I can only imagine ma defined a la ma func = let consts :: [r] consts = ... vals :: [a] vals = ... in combine consts (map func vals) so unless ma is constant (very uninteresting), f will in practice be indeed applied to values of type a which are in some sense 'extracted' from ma. Is that sufficiently close to what you mean or do I still not understand what you're trying to convey? Cheers, Daniel

On Sep 3, 2006, at 12:32 , Daniel Fischer wrote:

...

Am Sonntag, 3. September 2006 15:39 schrieb Lennart Augustsson:

...

Well, bind is extracting an 'a'. I clearly see a '\ a -> ...'; it getting an 'a' so it can give that to g. Granted, the extraction is very convoluted, but it's there.

-- Lennart

But

instance Monad (Cont r) where return = flip id (>>=) = (. flip) . (.) -- or would you prefer (>>=) = (.) (flip (.) flip) (.) ?

if we write it points-free. No '\a -> ...' around. And, being more serious, I don't think, bind is extracting an 'a' from m. How could it? m does not produce a value of type a, like a (State f) does (if provided with an initial state), nor does it contain values of type a, like [] or Maybe maybe do. And to my eyes it looks rather as though the '\a -> ...' tells us that we do _not_ get an 'a' out of m, it specifies to which function we will eventually apply m, namely 'flip g k'. But I've never really understood the Continuation Monad, so if I'm dead wrong, would you kindly correct me?

And if anybody knows a nontrivial but not too advanced example which could help understanding CPS, I'd be glad to hear of it.

Cheers, Daniel

On Fri, Sep 01, 2006 at 07:22:02AM +0200, Tomasz Zielonka wrote:

...

The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once)

How about using monad laws, specifically:

(return x) >>= f == f x

We assume that >>= never uses it's second argument, so:

(return x) >>= f == (return x) >>= g

Combining it with the above monad law we get:

f x == (return x) >>= f == (return x) >>= g == g x

so

f x = g x

for arbitrary f and g. Let's substitute return for f and undefined for g:

return x = undefined x

so

return x = undefined

Now that seems like a very trivial (and dysfunctional) monad.

I just realized that I haven't addressed your exact problem, but maybe you'll be able to use a similar reasoning to prove your theorem. What (I think) I proved is that: if >>= never uses its second argument, then the monad is dysfunctional (maybe not even a monad at all). Again, informally, it is obvious. Best regards Tomasz

Benjamin Franksen wrote:

Tomasz Zielonka wrote:

...

whatever you do, you won't be able to extract an 'a' typed value, non-bottom from this computation. Cont is defined as:

newtype Cont r a = Cont {runCont :: (a -> r) -> r)}

So getting the value out of the monad is not a pure function (extract :: Monad m => m a -> a). I think I stated that, already, in my previous post. I'd even say that the monadic values alone can be completely meaningless. They often have a meaning only relative to some environment, thus are (usually) _effectful_ computations. But we already knew that, didn't we?

The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once), and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value.

I think the continuation monad might help to refine the intuition: Cont a_r_r >>= a_C_b_r_r = Cont $ \ b_r -> a_r_r (\a -> runCont (a_C_b_r_r a) b_r) so it is clear that 1) The first computation (a_r_r x) might involve running the second (applying b_r_r to b_r) so it gives a counterexample to the idea that the first computation is run to completion before the second one starts, though it preserves the intuition that at least the first computation is started first. 2) The bind operation has arranged that value(s) of type (a) are supplied in the course of running the first computation to the second (in the "non-trivial" case where the second computation is actually run) Perhaps the argument could be that because the (a) is polymorphic, this implies that if the second computation is run at all, at least we know that the first computation has already started, and that the (a) came from the part of the first computation we've done so far, though of course this is still unfortunately very vague. Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com