How do I get the type of (sequence .) . fmap?

user_5587299 0
Viewed 226

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))
type-systems haskell
2 Answers

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)
user_54998710

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
user_38626980
Related