5

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))
6
  • 2
    Note that the function here is actually (.) ((.) sequence) fmap, so the . applies first on the sequence, not on the fmap. Commented Jan 10, 2019 at 14:35
  • @WillemVanOnsem, thanks! Seems I did substitution wrong :-(
    – aryndin
    Commented Jan 10, 2019 at 14:39
  • @WillemVanOnsem Can I substitute t (m a2) ~ ((a -> b) -> c)?
    – aryndin
    Commented Jan 10, 2019 at 14:42
  • You can get a second equation on b from the type of fmap . Then the two equations beginning b ~ will let you eliminate some of the other variables.
    – bergey
    Commented Jan 10, 2019 at 16:51
  • 1
    By the way, you can take a bit of a short cut to figuring this one out. (sequence .) . fmap = \f -> (sequence .) (fmap f) = \f -> sequence . fmap f = mapM f, and we know that mapM :: (Monad m, Traversable t) => (a -> m b) -> t a -> m (t b). If you used sequenceA instead, you'd end up with traverse instead, weakening the Monad constraint to an Applicative 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.
    – dfeuer
    Commented Jan 10, 2019 at 20:27

2 Answers 2

1

Let's keep our type variables all distinct.

(.)      ::                             (b -> c) -> (a -> b) -> a -> c
fmap     :: Functor f                => (u -> v) -> f u -> f v
sequence :: (Traversable t, Monad m) => t (m x)  -> m (t x)

We have two uses of the function .. I will use a1 and the like for the first one, and a2 and the like for the second one.

In (sequence .), we have (b1 -> c1) = (t (m x) -> m (t x)), so b1 = t (m x) and c1 = m (t x). Using substitution, . is specialized to (t (m x) -> m (t x)) -> (a1 -> t (m x)) -> a1 -> m (t x), and after being applied to sequence, we have a term of type (a1 -> t (m x)) -> a1 -> m (t x).

Now we can look at the second ., (sequence .) . fmap. Here, we have (b2 -> c2) = (a1 -> t (m x)) -> a1 -> m (t x), and (a2 -> b2) = (u -> v) -> f u -> f v.

This means that:

b2 = a1 -> t (m x)
c2 = a1 -> m (t x)
a2 = (u -> v)
b2 = f u -> f v

Notice that we have b2 up there twice, which means that a1 = f u and t (m x) = f v, so we can also derive that f = t, v = m x.

Now that we know all of those types, we know that the second . is specialized to

((t u -> t (m x)) -> (t u -> m (t x)) 
  -> ((u -> m x) -> (t u -> t (m x))) 
  -> (u -> m x) 
  -> (t u -> m (t x))

But we've already applied both of .'s arguments, so the whole expression's type is (u -> m x) -> (t u -> m (t x)).

And from there, it's just variable renaming, constraints, and parenthesis away from what ghci gives me.

> :t (sequence .) . fmap
(sequence .) . fmap
  :: (Monad m, Traversable t) => (a1 -> m a) -> t a1 -> m (t a)
1

It's late but still, I would like to answer.

These were the steps I took to understand .).

Actually It's not type inference that need, we Need to understand Substitution steps and type inference will just fallout.

as pointed in one comment, supposed substation is incorrect.

Substation steps for (sequence .) . fmap

  1. sequence . -- (.) composition operator takes sequence as left argument
  2. (sequence .) . -- outer (.) takes (sequence .) as left argument
  3. (sequence .) . fmap -- outer (.) takes fmap as right argument

Why we even need .). in first place

lets take a simple example what if I want to compose 2 functions first with two arguments and second with one

here I have taken simple example

i' :: Int -> Int -> String
i' x = show . (x +)

Substitution order

  1. show . -- (.) takes show as left argument
  2. x + -- (+) takes x as left argument
  3. show . (x +) -- (.) takes (x +) as right argument

What if we like to make is point free ?

here it is

i :: Int -> Int -> String
i = (show .) . (+)

Substitution order

  1. show . -- (.) takes show as left argument
  2. (show .) . -- outer (.) takes (show .) as left argument
  3. (show .) . (+) -- (.) takes (x) as right argument

We can even create an operator for it

(.~.) :: (b -> c) -> (a1 -> a2 -> b) -> a1 -> a2 -> c
f .~. g = (f .) . g -- wish I could name it (..)

and use it like this

f :: (Monad m, Traversable t) => (a1 -> m a) -> t a1 -> m (t a)
f = sequence .~. fmap

So .). is nothing but (f .) taking . g in right argument where g will take 2 argument.

BTW nothing is stopping us from

jj ::(Show b)=> (a1 -> a2 -> a3 -> b) -> a1 -> a2 -> a3 -> String
jj = (((show .) . ) . someFunctionWithThreeArguments

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.