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 Functor
s 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?
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 asa
, andEither a a
is the same asa
, and hence we just degenerate to asking whetherffmorph
is the only monoid homomorphisma -> b
. The answer is "no".For example, for the commutative monoid of addition, we have
replicate 'a' :: Either (Sum Int) (Sum Int) -> String
, where: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).