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
| haskell   | monads   2017-01-06 23:01 3 Answers

Answers ( 3 )

  1. 2017-01-07 00:01

    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')]
    
  2. 2017-01-07 03:01

    Addressing your edit, in which you consider how to write...

    \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. 2017-01-07 11:01

    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

    {-# 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.

◀ Go back