Hi Nicolas,
On 12/11/06, Nicolas Frisby
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 ->) monad, there types are:
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:
Prelude Control.Monad.Reader> :t liftM2 (-) snd fst 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 context meant a monadic computation in the (e ->) monad. Regards, Nick