Uniqueness of pure

Question

For any Applicative instance, once <*> is written, pure is uniquely determined. Suppose you have pure1 and pure2, both of which obey the laws. Then

pure2 f <*> pure1 y = pure1 ($ y) <*> pure2 f  -- interchange for pure1
pure2 id <*> pure1 y = pure1 ($ y) <*> pure2 id -- specialize f to id
pure1 y = pure1 ($ y) <*> pure2 id  -- identity for pure2
pure1 y = fmap ($ y) (pure2 id) -- applicative/fmap law for pure1
pure1 y = pure2 ($ y) <*> pure2 id -- applicative/fmap law for pure2
pure1 y = pure2 y -- homomorphism law

But using the fmap law this way feels like a cheat. Is there a way to avoid that without resorting to appeals to parametricity?

Answer 1

The laws as given in the current documentation do rely on parametricity to connect to fmap.

Without parametricity, we lose that connection, as we cannot even prove the uniqueness of fmap, and indeed there are models/extensions of System F where fmap is not unique.

A simple example of breaking parametricity is to add type-case (pattern-matching on types), this allows you to define the following twist which inspects the type of its argument and flip any boolean it finds:

twist :: forall a. a -> a
twist @Bool     = not
twist @(a -> b) = \f -> (\x -> twist @b (f (twist @a x)))
twist @a        = id  -- default case

It has the type of polymorphic identity, but it is not the identity function.

You can then define the following "twisted identity" functor, where pure applies twist to its argument:

newtype I a = I { runI :: a }

pure :: a -> I a
pure = I . twist

(<*>) :: I (a -> b) -> I a -> I b  -- The usual, no twist
(<*>) (I f) (I x) = I (f x)

A key property of twist is that twist . twist = id. This allows it to cancel out with itself when composing values embedded using pure, thus guaranteeing the four laws of Control.Applicative. (Proof sketch in Coq)

This twisted functor also yields a different definition of fmap, as \u -> pure f <*> u. Unfolded definition:

fmap :: (a -> b) -> I a -> I b
fmap f (I x) = I (twist (f (twist x)))

This does not contradict duplode's answer, which translates the usual argument for the uniqueness of the identity of monoids to the setting of monoidal functors, but it undermines its approach. The issue is that view assumes that you have a given functor already and that the monoidal structure is compatible with it. In particular, the law fmap f u = pure f <*> u is implied from defining pure as \x -> fmap (const x) funit (and (<*>) also accordingly). That argument breaks down if you haven't fixed fmap in the first place, so you don't have any coherence laws to rely on.

Answer 2

Let's switch to the monoidal functor presentation of applicative:

funit :: F ()
fzip :: (F a, F b) -> F (a, b)

fzip (funit, v) ~ v
fzip (u, funit) ~ u
fzip (u, fzip (v, w)) ~ fzip (fzip (u, v), w)

If we specialise a and b to () (and look past the tuple isomorphisms), the laws tell us that funit and fzip specify a monoid. Since the identity of a monoid is unique, funit is unique. For the usual Applicative class, pure can then be recovered as...

pure a = fmap (const a) funit

... which is just as unique. While in principle it makes sense to try to extend this reasoning to at least some functors that aren't fully parametric, doing so might require compromises in a lot of places:

• The availability of () as an object, to define funit and state the monoidal functor laws;

• The uniqueness of the map function used to define pure (see also Li-yao Xia's answer), or, failing that, a sensible way to somehow uniquely specify a fmap . const analogue;

• The availability of function types as objects, for the sake of stating the Aplicative laws in terms of (<*>).