I am trying to understand why adding id
in the last line of the sequence below removes the monadic aspect:
Prelude> :t id
id :: a -> a
Prelude> :t Control.Monad.liftM2
Control.Monad.liftM2
:: Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
Prelude> :t (==)
(==) :: Eq a => a -> a -> Bool
Prelude> :t Control.Monad.liftM2 (==)
Control.Monad.liftM2 (==)
:: (Monad m, Eq a) => m a -> m a -> m Bool
Prelude> :t Control.Monad.liftM2 (==) id
Control.Monad.liftM2 (==) id :: Eq a => (a -> a) -> a -> Bool
Prelude>
How does adding id :: a -> a
change the signature in the way it does in the last line ?
You’re fixing the type to a particular Monad
instance, namely the “function reader” monad (instance Monad ((->) a)
).
id :: a -> a
and you are attempting to use it as an argument to a parameter of type m a
, so:
m a ~ a -> a
m a ~ (->) a a
m a ~ ((->) a) a
m ~ (->) a
a ~ a
The remainder of the signature is:
m a -> m Bool
And since m ~ (->) a
, the resulting type is:
(->) a a -> (->) a Bool
(a -> a) -> (a -> Bool)
(a -> a) -> a -> Bool
(Plus the Eq a
constraint from the use of ==
.)
This is useful in pointfree code, particularly using the Applicative
instance, since you can implicitly “spread” the argument of a function to subcomputations:
nextThree = (,,) <$> (+ 1) <*> (+ 2) <*> (+ 3)
-- or
nextThree = liftA3 (,,) (+ 1) (+ 2) (+ 3)
nextThree 5 == (6, 7, 8)
uncurry' f = f <$> fst <*> snd
-- or
uncurry' f = liftA2 f fst snd
uncurry' (+) (1, 2) == 3
The signature of liftM2 (==)
is (Monad m, Eq a) => m a -> m a -> m Bool
. So that means that if we call this function with id :: b -> b
as argument, then it means that m a
and b -> b
are the same type.
The fact that m ~ (->) b
holds is not a problem since (->) r
is an instance of Monad
, indeed in the GHC.Base source code we see:
-- | @since 2.01 instance Monad ((->) r) where f >>= k = \ r -> k (f r) r
This only makes sense if m ~ (->) b
. Here the arrow (->)
is a type constructor, and (->) a b
is the same as a -> b
.
So it means that if we calculate the type of liftM2 (==) id
, we derive the following:
liftM2 (==) :: m a -> m a -> m Bool
id :: (b -> b)
-------------------------------------------
m ~ (->) b, a ~ b
This thus means that the output type of liftM2 (==) id
is liftM2 (==) id :: (Monad m, Eq a) => m a -> m Bool
, but we need to "specialize" this with the knowledge we obtained: that m a
is (->) b
and a
is the same type as b
, so:
liftM2 (==) id :: (Monad m, Eq a) => m a -> m Bool
-> liftM2 (==) id :: (Monad m, Eq a) => (b -> a) -> (b -> Bool)
-> liftM2 (==) id :: Eq b => (b -> b) -> (b -> Bool)
-> liftM2 (==) id :: Eq b => (b -> b) -> b -> Bool
In short the function is still "monadic", although by using id
, you have selected a specific monad, and thus the function is no longer applicable to all sorts of monads, only to the (->) r
monad.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With