What can be proved about parameters in lambda expressions, passed into monads?

Question

Relative to the fish operator, Monads satisfy associativity.

``````(h >=> g) >=> f = h >=> ( g >=> f)
``````

This translated to bind (with lambda expressions) looks like,

``````\a -> h a >>=(\b -> g b >>= \c -> f c) =
\a ->(h a >>= \b -> g b)>>= \c -> f c
``````

which means the following equation is unambiguous

``````( a -> h a >>= \b -> g b >>= \c -> f c ) =  h >=> g >=> f
``````

This is a nice way to understand Monadic composition.

However not all Monadic code keeps the bound variables to the lambdas separated. For example,

``````[1,2] >>= \n -> ['a','b'] >>= \ch -> return (n,ch) =
[(1,'a'),(1,'b'),(2,'a'),(2,'b')]
``````

The "n" in the return was obtained from the top lambda.

More generally,

``````a -> g a >>= \b -> f a b
``````

f depends on both a and b in the above. Defining the above in terms of f, g, and (>=>) gives

``````\a -> (\x -> g a) >=> f a
``````

Which I don't understand very well. It doesn't match the above equation I showed very well. I see fish as the fundamental notion here, and I'm trying to understand how it interacts with typical Monads I write. I would like to understand the above better.

One way of approaching this is by trying to obtain meaning from List expression syntax

``````[ (n,ch) | n <- [1, 2], ch <- ['a', 'b'] ]
``````

I think this implies a kind of symmetry.

Are there any nice symmetries connecting lambda expressions and Monads? Or am I reading too much into this? Is my fear of highly nested lambda expressions wrong or reasonable?

Show source

Answers to What can be proved about parameters in lambda expressions, passed into monads? ( 3 )

1. No, there aren't any restrictions. Once you've bound a lambda you can do anything. This is one of the reasons of `Applicative` being preferrable to `Monad` because it's weaker (and hence gives you stronger free-theorem restrictions).

`````` ( [1,2] >>= \n -> "ab" >>= \ch -> return (n,ch) )
≡  (,) <\$> [1,2] <*> "ab"
≡  liftA2 (,) [1,2] "ab"
≈  liftA2 (flip (,)) "ab" [1,2]
``````

The last is actually not a proper equation; the applicative laws only guarantee that the values will be the same for these expressionsSee comments, but the structure can and will be different.

``````Prelude Control.Applicative> liftA2 (,) [1,2] "ab"
[(1,'a'),(1,'b'),(2,'a'),(2,'b')]
Prelude Control.Applicative> liftA2 (flip (,)) "ab" [1,2]
[(1,'a'),(2,'a'),(1,'b'),(2,'b')]
``````

``````\a -> g a >>= \b -> f a b
``````

... using `(>=>)`, nothing is actually lost in that case. It is helpful to take a step back and consider exactly how `(>=>)` can be converted into `(>>=)` and vice-versa:

``````f >=> g = \x -> f x >>= g
m >>= f = (const m >=> f) () -- const x = \_ -> x
``````

In the second equation, which is the one related to your concerns, we turn the first argument to `(>>=)` into a function which can be passed to `(>=>)` by using `const`. As `const m >=> f` is a functions which ignores its argument, we just pass `()` as a dummy argument in order to recover `(>>=)`.

That being so, your example can be rewritten by using the second equation:

``````\a -> g a >>= \b -> f a b
\a -> (const (g a) >=> \b -> f a b) ()
\a -> (const (g a) >=> f a) ()
``````

Which, except for the added trick of supplying a dummy `()`, is what you had obtained in your question.

3. An additional idea to your question: Monads are most general in the sense that effects can depend on inputs. A monadic computation `m` that takes input `a` and produces output `b` can be written as `a -> m b`. As this is a function, we (can) define such computations using lambdas, which can naturally span fo the right. But this generality complicates analyzing computations as your `\a -> g a >>= \b -> f a b`.

For arrows (which occupy the space between applicative functors and monads) the situation is somewhat different. For a general arrow, the input must be explicit - an arrow computation `arr` has the general type of `arr a b`. And so an input that spans "forward" in an arrow computation must be explicitly threaded there using Arrow primitives.

``````{-# LANGUAGE Arrows #-}

import Control.Arrow

bind2 :: (Monad m) => (a -> m b) -> (a -> b -> m c) -> a -> m c
bind2 g f = \a -> g a >>= \b -> f a b
``````

to arrows: Function `f` must now take a pair as its input (because arrows are defined as accepting one input value). Using the arrow `do` notation we can express it as

``````bind2A :: (Arrow arr) => arr a b -> arr (a, b) c -> arr a c
bind2A g f = proc a -> do
b <- g -< a
c <- f -< (a, b)
returnA -< c
``````

Or even simpler using the `Arrow` primitives:

``````bind2A' :: (Arrow arr) => arr a b -> arr (a, b) c -> arr a c
bind2A' g f = (returnA &&& g) >>> f
``````

Graphically:

``````--------------->[   ]
\            [ f ]---->
\-->[ g ]-->[   ]
``````

Being less general, arrows allow to infer more information about a circuit before it's actually executed. A nice reading is Understanding arrows, which describes the original motivation behind them - to construct parsers that can can avoid space leaks by having static and dynamic parts.