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

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 ( 3 )

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).The last is actually not a proper equation; the applicative laws only

~~guarantee that the~~valueswill be the same for these expressions^{See comments}, but thestructurecan and will be different.Addressing your edit, in which you consider how to write...

... 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: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:

Which, except for the added trick of supplying a dummy

`()`

, is what you had obtained in your question.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.To expand your example

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 asOr even simpler using the

`Arrow`

primitives:Graphically:

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.