Nicola Paolucci durden at gmail.com
Mon Dec 11 18:54:45 EST 2006

```Hi Nicolas,

On 12/11/06, Nicolas Frisby <nicolas.frisby at gmail.com> wrote:
> The interpreter infers that m = (e ->) because of the types of snd and fst.
>
> When snd and fst are considered as monadic computations in the (e ->)
>
> Prelude> :t fst
> fst :: (a, b) -> a
> Prelude> :t snd
> snd :: (a, b) -> b
>
> Note that: (a, b) -> a =~= m a    where m x = (a,b) -> x
>
> So if we apply liftM2 to fst and snd, then the m of the result has to
> be the same as the m of the arguments; thus the m of the result is
> ((a, b) ->). Now the type of (-) is:
>
> Prelude> :t (-)
> (-) :: (Num a) => a -> a -> a
>
> Thus the interpreter knows that the a and b in the ((a, b) ->) monad
> are actually the same. Finally we have:
>
> liftM2 (-) snd fst :: (Num a) => (a, a) -> a
>
> Note that: (a, a) -> a =~= m a    where m x = (a,a) -> x
>
> So each argument to liftM2 contributes constraints to the components
> of liftM2's general type:
>
> Prelude> :t liftM2
> liftM2 :: (Monad m) => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
>
> snd forces m to be ((x,a2) ->)
> fst forces m to be ((a1,y) ->)
> (-) forces a1 and a2 to be the same
>
> The conjunction of these contraints forces {a1:=a, a2:=a, m:=(a,a) ->}.

Really clearly exposed.

Thanks a lot, it all starts to make perfect sense.
The main point I was missing I now realize was that m in my example