I try to understand how Haskell type inference and type system works. Now I'm studying the case of (sequence .) . fmap
. I get types of (sequence .)
and (. fmap)
as haskell does:
(.) :: (b -> c) -> (a -> b) -> a -> c
fmap :: Functor f => (a -> b) -> f a -> f b
sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)
-- Type for . fmap:
a ~ (a -> b)
b ~ (f a -> f b)
. fmap :: ((f a -> f b) -> c) -> ((a -> b) -> c)
-- Type for sequence:
b ~ t (m a1)
c ~ m (t a2)
sequence . :: (a1 -> t (m a2)) -> (a1 -> m (t a2))
But then I can't get the type of (sequence .) . fmap
. I tryed following steps and then stucked:
(sequence .) . fmap - ?
f a ~ a1
f b ~ t (m a2)
b ~ m a2
c ~ (a1 -> m (t a2))
(sequence .) . fmap :: (a -> m a2) -> (a1 -> m (t a2))
The type I've got differs from the one haskell give.
UPD Thanks to @WillemVanOnsem, I've got some progress, but then stucked again...
(.) :: (b -> c) -> (a -> b) -> a -> c
(fmap) :: Functor f => (z -> u) -> f z -> f u
sequence . :: (a1 -> t (m a2)) -> (a1 -> m (t a2))
b ~ (a1 -> t (m a2))
c ~ (a1 -> m (t a2))
a ~ (z -> u)
(sequence .) . fmap :: ((a1 -> t (m a2)) -> (a1 -> m (t a2))) ->
((z -> u) -> (a1 -> t (m a2))) ->
((z -> u) -> (a1 -> m (t a2))
(.) ((.) sequence) fmap
, so the.
applies first on thesequence
, not on thefmap
.t (m a2) ~ ((a -> b) -> c)
?b
from the type offmap
. Then the two equations beginningb ~
will let you eliminate some of the other variables.(sequence .) . fmap = \f -> (sequence .) (fmap f) = \f -> sequence . fmap f = mapM f
, and we know thatmapM :: (Monad m, Traversable t) => (a -> m b) -> t a -> m (t b)
. If you usedsequenceA
instead, you'd end up withtraverse
instead, weakening theMonad
constraint to anApplicative
one. Even if you don't want to take that shortcut, transforming to the lambda form I showed will very likely help you work out the type more directly.