Functoriality law is a free theorem

[masaeedu]

The law labeled "functoriality" in the Semialign class is a free theorem.

Here is the law as written:

f1, f2 :: Semialign f => (a -> c) -> (b -> d) -> f a -> f b -> f (These c d)
f1 f g x y = align (f <$> x) (g <$> y)
f2 f g x y = bimap f g <$> align x y

-- "Functoriality"
-- f1 = f2

Uncurry the arguments:

f1, f2 :: Semialign f => (a -> c) -> (b -> d) -> (f a, f b) -> f (These c d)
f1 f g (x, y) = align (f <$> x) (g <$> y)
f2 f g (x, y) = bimap f g <$> align x y

Eta reduce:

f1, f2 :: Semialign f => (a -> c) -> (b -> d) -> (f a, f b) -> f (These c d)
f1 f g = uncurry align . bimap (fmap f) (fmap g)
f2 f g = fmap (bimap f g) . uncurry align

Explicitly write composite functors:

bimapBiff :: (Bifunctor t, Functor f, Functor g) => (a -> c) -> (b -> d) -> t (f a) (g b) -> t (f c) (g d)
bimapBiff f g = bimap (fmap f) (fmap g)

bimapTannen :: (Bifunctor t, Functor f) => (a -> c) -> (b -> d) -> f (t a b) -> f (t c d)
bimapTannen f g = fmap (bimap f g)

f1, f2 :: Semialign f => (a -> c) -> (b -> d) -> (f a, f b) -> f (These c d)
f1 f g = uncurry align . bimapBiff f g
f2 f g = bimapTannen f g . uncurry align

In other words, the law simply demands that align :: Biff (,) f f a b -> Tannen f These a b is a natural transformation between the bifunctors Biff (,) f f and Tannen f These.

This is a free theorem: every parametrically polymorphic function of the type foo :: forall a b. T a b -> U a b, where T and U are bifunctors, is a natural transformation between those bifunctors.

Like any other free theorem, it can be violated by doing naughty stuff with partiality and laziness in Haskell, but if we ignore those pathological cases the law is inviolable.

[phadej]

Or with GADTs.

[phadej]

More wordly:

The composition Functor law fmap (f . g) = fmap f . fmap g is similarly implied by fmap id = id and free theorem, but there's still point in stating that law. It can be broken without partiality and laziness, GADTs can be non-parameteric and non-natural, and therefore free theorems won't hold.

[masaeedu]

@phadej Can you show an example of a GADT that violates the law without relying on partiality and laziness? There is a long discussion on a similar topic here: https://stackoverflow.com/a/60384830, and I remain unconvinced that there is a way to break parametricity merely with the use of existential types.

[phadej]

Mag mentioned in https://ryanglscott.github.io/2018/06/22/quantifiedconstraints-and-the-trouble-with-traversable/ and https://github.com/ekmett/bifunctors/blob/ffc6b5c0a7fe8f3e1c3603e54a4025f06d7bcfba/src/Data/Biapplicative.hs#L212-L222

[masaeedu]

Yes, Mag is indeed mentioned in that blog post. What about it?

[phadej]

Sorry, I should asked the following right in the beginning:

What is the issue? What one need to do to resolve it?

---

Mag is an example of a type which breaks parametricity.

[masaeedu]

The issue is that the functoriality law is implied by the laws of functors and the type system, so in most situations it is not a law the user needs to worry about when writing an instance, as they do for the other laws. It would be good to distinguish this in the documentation, as is done for example in the documentation for the selective functor library: https://hackage.haskell.org/package/selective-0.4.1/docs/Control-Selective.html.

Can you flesh out what you mean regarding Mag? I still don't see a way in which that type violates parametricity.

[masaeedu]

If I were to guess I think you're pointing to the fact that fmap id /= id, but it's also the case that fmap (f . g) /= fmap f . fmap g for that type, so I don't really understand what this is supposed to prove about violating free theorems.

The statement about parametricity that's relevant to the issue we're discussing is that for any two functors F and G, a function of the type forall a. F a -> G a is automatically a natural transformation between them. If you have an example of a GADT that violates this, then obviously this statement is wrong and I need to reconsider the utility of free theorems, but I haven't seen one thus far.

[phadej]

It would be good to distinguish this in the documentation,

Please make a PR.

[phadej]

Note: I include the naturality law, because in Haskell it (might be often / always is) true. But in more general setting it wouldn't.

For Functor specifying fmap (f . g) = fmap f . fmap g is not necessary either. You cannot break that law with parameteric type, without also breaking fmap id = id one too.

[masaeedu]

For Functor specifying fmap (f . g) = fmap f . fmap g is not necessary either. You cannot break that law with parameteric type, without also breaking fmap id = id one too.

That's what I'm talking about. If the fmap id = id law held but fmap (f . g) = fmap f . fmap g didn't then this would illustrate a violation of the free theorem for fmap. However neither law holds for that type, so I don't see how this is relevant to a discussion of free theorems and whether or not they hold in the presence of GADTs.

[phadej]

There is no note that the latter composition fmap (f . g) = fmap f . fmap g holds for free if fmap id holds. Even there are blogs post about that (e.g. https://www.schoolofhaskell.com/user/edwardk/snippets/fmap)

I argue that there is really no benefit in omitting stating naturality laws. It might make sense to mention that you need to do suspicious things to break them, but they should be in the documentation.

I still don't undestand what and how you try to improve. Please make a PR = concrete change proposal.