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?

Selfpity

Intriguing. I'm sure something could be said about this in the light of <*> being not really the “fundamental” method of applicative, i.e. monoidal functors – it's rather fzip :: f a -> f b -> f (a,b). However, I just don't quite get what you mean by “feels like a cheat”. You're just using the laws, how can that be a cheat. – Claimant

@leftaroundabout, I guess what I really mean is that the uniqueness of fmap (which implies the fmap/Applicative law) flows from parametricity. So if you take these laws out of a context where parametricity holds, that raises the question of whether pure is still determined by <*> or whether it's actually determined only by the combination of fmap with <*>. – Selfpity

I was also wondering how fzip and funit :: f () might play into this sort of question. – Selfpity

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.

Beck

That's a very nicely presented example of parametricity breaking. When I originally wrote my answer, I hoped to keep an opening for not fully parametric functors which nonetheless would have an unique map function. The funit/pure connection doesn't tend to translate well to such settings, though. – Corner

" type-case (pattern-matching on types)" is that different to making twist a class/method and using instances to achieve pattern-matching on types? – Vasty

Your twist . twist = id is similar to double reverse, in which (reverse . f) . (reverse . g) =/= (reverse . (f . g)) over here #66136123 – Vasty

you could use a class to define something similar but that seems besides the point of the question about parametricity and the Applicative class. – Beck

Why do you need to assume finiteness or extra machinery? Won't a default (identity) case do the trick? – Selfpity

I think a class should be fine. Either way, I think I get the drift, though I'd prefer an informal proof to one based on Coq tactics (which I don't know how to read). – Selfpity

Right, I include that mostly to say "someone did the proof at least once" and to avoid putting people who want to see the proof for themselves on a wild-goose chase. – Beck

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 (<*>).

Corner

So it sounds like the Functor instance may be necessary to link those presentations? – Selfpity

@Selfpity Perhaps that can be avoided. For instance, it should work fine with Data.Set.map . const instead of (<$). The question which lies behind the "should", I guess, is what exactly does it take for there to be a sensible analogue of (<$) if we can't rely on parametricity. (By the way, note that, on second thought, I have somewhat weakened the closing words of the answer.) – Corner

@Selfpity In any case, Data.Set is a somewhat questionable example, as insisting on the Ord constraint costs us a straightforward analogue to (<*>). It seems most examples I can think of are questionable in one way or another... – Corner