`(<*>)` definition for the Applicative functor?

Question

Some Haskell source code (see ref):

-- | Sequential application.
--
-- A few functors support an implementation of '<*>' that is more
-- efficient than the default one.
(<*>) :: f (a -> b) -> f a -> f b
(<*>) = liftA2 id

-- | Lift a binary function to actions.
--
-- Some functors support an implementation of 'liftA2' that is more
-- efficient than the default one. In particular, if 'fmap' is an
-- expensive operation, it is likely better to use 'liftA2' than to
-- 'fmap' over the structure and then use '<*>'.
liftA2 :: (a -> b -> c) -> f a -> f b -> f c
liftA2 f x = (<*>) (fmap f x)

Three things seem to be quite confusing to me:

1) (<*>) is defined in terms of liftA2, where liftA2 is defined in terms of (<*>). How does it work? I see no obvious "recursion-break" case...

2) id is an a -> a function. Why is it passed into liftA2 as an (a -> b -> c) function?

3) fmap id x always equals x, since functors must preserve appropriate identities. Thus (<*>) (fmap id x) = (<*>) (x) where x = f a - an a-typed functor itself (by the way, how can a-typifying of the functor can be explained from the pure category theory's point of view? functor is just a mapping between categories, it has no further "typification"... seems like it is better to say - "a container of type a with an (endo)functor defined for each instance of asummed category Hask of well-defined Haskell types). So (<*>) (f a) while by definition (<*>) expects f(a' -> b'): thus, the only way to make it work is to deliberately bound a to be an (a' -> b'). However when I run :t \x -> (<*>) (fmap id x) in the gchi, it spits out something mind-blowing: f (a -> b) -> f a -> f b - which I fail to explain.

---

Can someone step by step explain how does that work and why it even compiles? P.S. Category theory terms, if needed, are welcome.

Answer 1

For question 1, you left out a very important piece of context.

class Functor f => Applicative f where
    {-# MINIMAL pure, ((<*>) | liftA2) #-}

Those definitions you quoted belong to a class. That means instances can override them. Furthermore, the MINIMAL pragma says that in order to work, at least one of them must be overridden in the instance. So the breaking of the recursion happens whenever one is overridden in a particular instance. This is just like how the Eq class defines (==) and (/=) in terms of each other so that you only need to provide a definition for one in a hand-written instance.

For question two, a -> b -> c is shorthand for a -> (b -> c). So it unifies with (let's rename variables to avoid collision) d -> d as (b -> c) -> (b ->c). (tangentially, that's also the type of ($).)

For three - you're absolutely right. Keep simplifying!

\x -> (<*>) (fmap id x)
\x -> (<*>) x
(<*>)

So it shouldn't really be a surprise ghci gave you the type of (<*>) back, should it?

Answer 2

1) (<*>) is defined in terms of liftA2, where liftA2 is defined in terms of (<*>). How does it work? I see no obvious "recursion-break" case...

It's not recursion. In your instance of Applicative you can either define both of them or just one. If you define just (<*>) then liftA2 is defined from (<*>), and vice versa.

2) id is an a -> a function. Why is it passed into liftA2 as an (a -> b -> c) function?

Unification works as follows,

(<*>) :: f (a -> b) -> f a -> f b
(<*>) = liftA2 id

liftA2 :: (a -> b -> c) -> f a -> f b -> f c

id     :  u -> u 
liftA2 : (a -> (b -> c) -> f a -> f b -> f c
------------------------------------------------------
u = a
u = b->c

id     :  (b->c) -> (b->c)
liftA2 : ((b->c) -> (b->c)) -> f (b->c) -> f b -> f c
------------------------------------------------------

liftA2 id : f (b->c) -> f b -> f c

3.

liftA2 :: (a -> b -> c) -> f a -> f b -> f c
liftA2 h x = (<*>) (fmap h x)

Renamed the first argument from f to h, to prevent confusion since f also shows in the type

h    :: a -> (b -> c)
x    :: f a
fmap :: (a -> d) -> f a -> f d
------------------------------
d  = b -> c
h    :: a -> (b->c)
x    :: f a
fmap :: (a -> (b->c)) -> f a -> f (b->c)
----------------------------------------
fmap h x :: f (b -> c)


fmap h x :: f (b -> c)
(<*>)    :: f (b -> c) -> f b -> f c
-------------------------------------
(<*>) fmap h x  :: f b -> f c

---

Edit:

Consistency

To show the consistency of both formulas, first lets first rewrite liftA2 into something simpler. We can use the formula below to get rid of fmap and use only pure and <*>

fmap h x = pure h <*> x

and it's best to put all points in the definition. So we get,

  liftA2 h u v  
= (<*>) (fmap h u) v
= fmap h u <*> v
= pure h <*> u <*> v

So we want to check the consistency of,

u <*> v      = liftA2 id u v 
liftA2 h u v = pure h <*> u <*> v

For the first we need the property that pure id <*> u = u

  u <*> v 
= liftA2 id u v 
= pure id <*> u <*> v
= u <*> v

For the second we need a property of liftA2. Properties of applicative are usually given in terms of pure and <*> so we need to derive it first. The required formula is derived from pure h <*> pure x = pure (h x).

  liftA2 h (pure x) v 
= pure h <*> pure x <*> v 
= pure (h x) <*> v
= liftA2 (h x) v   

This requires h : t -> a -> b -> c. The proof of consistency becomes,

  liftA2 h u v 
= pure h <*> u <*> v
= pure h `liftA2 id` u `liftA2 id` v   
= liftA2 id (liftA2 id (pure h) u) v 
= liftA2 id (liftA2 h u) v 
= liftA2 h u v 

Answer 3

1) (<*>) is defined in terms of liftA2, where liftA2 is defined in terms of (<*>). How does it work? I see no obvious "recursion-break" case...

Each instance is responsible for overriding at least one of the two. This is documented in a machine-readable way in the pragma at the top of the class:

{-# MINIMAL pure, ((<*>) | liftA2) #-}

This pragma announces that instance writers must define at least the pure function and at least one of the other two.

id is an a -> a function. Why is it passed into liftA2 as an (a -> b -> c) function?

If id :: a -> a, we can choose a ~ d -> e to get id :: (d -> e) -> d -> e. Traditionally, this particular specialization of id is spelled ($) -- maybe you've seen that one before!

3) ...

I don't... actually see any contradiction set up in the facts you state. So I'm not sure how to explain away the contradiction for you. However, you have a few infelicities in your notation that might be related to mistakes in your thinking, so let's talk about them briefly.

You write

Thus (<*>) (fmap id x) = (<*>) (x) where x = f a.

This is not quite right; the type of x is f a for some Functor f, but it is not necessarily equal to f a.

by the way, how can a-typifying of the functor can be explained from the pure category theory's point of view? functor is just a mapping between categories, it has no further "typification"... seems like it is better to say - "a container of type a with an (endo)functor defined for each instance of assumed category Hask of well-defined Haskell types

A functor constitutes two things: a mapping from objects to objects, and a mapping from arrows to arrows that is compatible with the object mapping. In a Haskell Functor instance declaration like

instance Functor F where fmap = fmapForF

the F is the mapping from objects to objects (objects in both the source and target categories are types, and F is a thing which takes a type and produces a type) and the fmapForF is the mapping from arrows to arrows.

I run :t \x -> (<*>) (fmap id x) in the gchi, it spits out something mind-blowing: f (a -> b) -> f a -> f b - which I fail to explain.

Well, you already observed that fmap id x = x, which means \x -> (<*>) (fmap id x) = \x -> (<*>) x. And for any function f, f = \x -> f x (up to some niggles that aren't important right now), so in particular \x -> (<*>) (fmap id x) = (<*>). So ghci gives you the type of (<*>), as it should.

Answer 4

Here I have to disagree with the GHC devs on their coding style :)

I would like to argue that one should never write

ap = liftA2 id

but, instead, use the equivalent

ap = liftA2 ($)

since the latter makes it clear that we are lifting the application operation.

(Actually, for very technical reasons GHC devs can not use $ here in this internal module, as pointed out below in the comments. So, at least they have a very good reason for their choice.)

Now, you might wonder why id can be used instead of $. Formally, we have

($) f x
= f x
= (id f) x
= id f x

hence, eta-contracting x then f, we get ($) = id.

Indeed, ($) is a "special case" of id.

id :: a -> a
-- choose a = (b -> c) as a special case
id :: (b -> c) -> (b -> c)
id :: (b -> c) -> b -> c
($):: (b -> c) -> b -> c

Hence, the main difference is: id is the identity on any type a, while ($) is the "identity" on any functional type b -> c. The latter is best visualized as a binary function (application), but it can equivalently be considered a unary function (identity) on a function type.