Is the only `FlippyFloppyMorphism` `const mempty`?

85 views Asked by At

In Haskell, we have the interesting fact that any type constructor f :: * -> * which is simultaneously a Functor and a Contravariant is phantom in its type parameter:

phantom :: (Functor f, Contravariant f) => f x -> f y

Another way to put this is that every type constructor that is simultaneously a Functors and a Contravariant is naturally isomorphic to Const x, for some x.

This implies that the "only" way (up to isomorphism) to instantiate the class:

class FlippyFloppyFunctor f
  where
  ffmap :: Either (y -> x) (x -> y) -> f x -> f y

so that it obeys the functor laws:

ffmap (Left id)       = id
ffmap (Right id)      = id
ffmap (Left  (g . f)) = ffmap (Left f)  . ffmap (Left g)
ffmap (Right (f . g)) = ffmap (Right f) . ffmap (Right g)

is:

weirdmap :: Either (y -> x) (x -> y) -> Const r x -> Const r y
weirdmap = const $ \(Const x) -> Const x

i.e. modulo newtypes, const id.

I find it difficult to understand why this is the only function of its type that satisfies the constraints, although I can sort of understand various informal arguments involving absurd :: Void -> a/discard :: a -> () as to why the existence of such a map implies the functor "is phantom" in its type parameter.

To understand it better, I tried to simplify the problem. Instead of thinking about FlippyFloppyFunctor, let's think about:

class (Monoid a, Monoid b) => FlippyFloppyMorphism a b
  where
  ffmorph :: Either a a -> b

with analogous laws:

ffmorph (Left mempty)    = mempty
ffmorph (Right mempty)   = mempty
ffmorph (Left  (y <> x)) = ffmorph (Left x)  <> ffmorph (Left y)
ffmorph (Right (x <> y)) = ffmorph (Right x) <> ffmorph (Right y)

Assuming that a and b are non-commutative monoids, is it still true that the only lawful implementation of FlippyFloppyMorphism is const mempty? Is it still possible to explain why the morphism must be "phantom" in the input monoids, without having a Void or a () to refer to?

1

There are 1 answers

4
Asad Saeeduddin On

It seems to me that the answer in the general case is "no", because monoids can be commutative.

If the monoid is commutative, then Dual a is the same monoid as a, and Either a a is the same as a, and hence we just degenerate to asking whether ffmorph is the only monoid homomorphism a -> b. The answer is "no".

For example, for the commutative monoid of addition, we have replicate 'a' :: Either (Sum Int) (Sum Int) -> String, where:

replicateA (Left  0) = ""
replicateA (Right 0) = ""
replicateA (Left  (y + x)) = replicateA (Left x) ++ replicateA (Left y)
replicateA (Right (x + y)) = replicateA (Left x) ++ replicateA (Left y)

However, I think it might be the case that for _non_commutative monoids, the only possible implementation is const mempty (which I still don't have a proof for).