Understanding the type of (,) <$> length <*> head

Question

I have this pair of functions

(,) <$> length :: Foldable t => t a -> b -> (Int, b)

and,

head :: [a] -> a

I would like to understand the type of

(,) <$> length <*> head

In (<*>) :: Applicative f => f (a -> b) -> f a -> f b type signature,

f :: (->) [a]

a :: b

b :: (Int -> b)

So, the instantiated type would be:

(->) [a] (Int, b)

However, I found out really its type is:

(->) [a] (Int, a)

Two questions, if I may:

• Why is the b switched for an a ?
• What's the step by step process in this type signature calculation ?

Answer 1

Let's keep using the signature

(,) <$> length :: Foldable t => t a -> b -> (Int, b)

But change

(<*>) :: Applicative f => f (a -> b) -> f a -> f b

to

(<*>) :: Applicative f => f (x -> y) -> f x -> f y

so it doesn't get confusing. Clearly f ~ (->) [a] (assuming we're using the list instance of foldable) as you noticed, and thus x -> y ~ b -> (Int, b), so x ~ b and y ~ (Int, b). This is the part you missed, likely due to having confusing naming: the second argument is f x or [a] -> b, and you pass in head, which is [a] -> a. This forces b to become the same as a, otherwise the types wouldn't work out. The result is f y, or [a] -> (Int, b), except b is now a, giving you the [a] -> (Int, a) signature.

Answer 2

One way to derive the type of (,) <$> length <*> head is to abstract over length and head and consider instead the resulting lambda expression

\l -> \h -> (,) <$> l <*> h

of type

Applicative f => f a -> f b -> f (a, b)

with the types [x] -> Int and [x] -> x of length and head respectively we require

f a ~ [x] -> Int
f b ~ [x] -> x

and thus

f ~ (->) [x]  -- hom-functor aka Reader 
a ~ Int
b ~ x

which yields

([x] -> Int) -> ([x] -> x) -> ([x] -> (Int, x))

as type for the above lambda expression.

Answer 3

Another way to derive the type of (,) <$> length <*> head is to work it out progressively by applying the definitions at every step:

(,)                     ::        a   ->       b -> (a, b) 
-- (<$>)                ::       (a   ->         c        ) -> f a -> f c
(,) <$>                 :: f      a   -> f    (b -> (a, b)) -- f a -> f c
--      length          :: [t] -> Int
(,) <$> length          ::             [t] -> (b -> (Int, b))
--            (<*>)     ::             f      (s -> q        ) -> f s -> f q
(,) <$> length <*>      ::  ([t] -> b) -> ([t] -> (Int, b))    -- f s -> f q
--                 head ::   [t] -> t
(,) <$> length <*> head ::                 [t] -> (Int, t)

The trickiest part is to correctly apply (->) [t] for f in the third and fourth step.

Answer 4

We can try to arrive at some more easily understood formulation first, so that its type becomes "obvious". We have

       (,) <$> length <*> head
=
pure   (,) <*> length <*> head
=
liftA2 (,)     length     head

for any Applicative, by the Applicative laws and the definition of liftA2.

So we have (,) combining the contained / carried / produced results from the applicative values length and head:

              (,)
             /   \
            /     \
       length      head

But length and head are functions, and for functions we have

              (,)
             /   \
            /     \
       length      head
            \     /
             \   /
               x

i.e.

liftA2 (,)     length     head   x
=
       (,)    (length x) (head   x)

by the definition of the (->)'s Applicative instance.

Thus the type of (,) <$> length <*> head is the type of liftA2 (,) length head is the type of \ x -> (length x , head x). And that is "obviously" "just" [a] -> (Int , a).

GHCi concurs:

> :t \ x -> (length x , head x)
\ x -> (length x , head x) :: [t] -> (Int, t)

> :t (,) <$> length <*> head
(,) <$> length <*> head    :: [a] -> (Int, a)

length :: Foldable t => t a -> Int is defined for any Foldable but head :: [a] -> a works on lists specifically, so length's type becomes specialized as [a] -> Int.

And head produces the same type that the elements of the input list have:

            (Int,a)        ~     (,) Int   a
             /   \                    |    |
            /     \                   |    |
       length      \       :: [a] -> Int   |
           \      head     :: [a] ->       a
            \     /            |
             \   /             |
              [a]          ~  [a]

So there's no "switching". Everything flows.