Ist der einzige "FlippyFloppyMorphism" "const mempty"?

Question

In Haskell haben wir die interessante Tatsache, dass jeder Typkonstruktor, f :: * -> *der gleichzeitig a Functorund a Contravariantist, in seinem Typparameter ein Phantom ist:

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

Ein anderer Weg, dies auszudrücken, ist, dass jeder Typkonstruktor, der gleichzeitig a Functors und a Contravariantist Const x, für einige von Natur aus isomorph ist x.

Dies impliziert, dass der "einzige" Weg (bis zum Isomorphismus) die Klasse instanziiert:

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

damit es den Funktorgesetzen gehorcht:

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)

ist:

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

dh Modulo Newtypes , const id.

Ich finde es schwierig zu verstehen , warum dies die einzige Funktion dieser Art ist , dass erfüllt die Einschränkungen, obwohl ich irgendwie verschiedenen informellen Argumente verstehen Beteiligung absurd :: Void -> a/ discard :: a -> (), warum die Existenz einer solchen Karte impliziert die Funktors „ist Phantom“ in seiner Art Parameter.

Um es besser zu verstehen, habe ich versucht, das Problem zu vereinfachen. Anstatt darüber nachzudenken FlippyFloppyFunctor, denken wir über:

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

mit analogen Gesetzen:

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)

Unter der Annahme , dass aund b sind nichtkommutative Monoide , ist es immer noch wahr , dass die einzige rechtmäßige Umsetzung FlippyFloppyMorphismist const mempty? Ist es immer noch möglich zu erklären, warum der Morphismus in den Eingangsmonoiden "Phantom" sein muss, ohne ein Voidoder ein ()zu haben, auf das Bezug genommen werden muss?

Answer 1

Es scheint mir, dass die Antwort im allgemeinen Fall "nein" ist, weil Monoide kommutativ sein können.

Wenn das Monoid kommutativ ist, dann Dual aist es dasselbe Monoid wie aund Either a adasselbe wie a, und daher degenerieren wir nur zu der Frage, ob dies ffmorphder einzige Monoidhomomorphismus ist a -> b. Die Antwort ist nein".

Zum Beispiel haben wir für das kommutative Additionsmonoid Folgendes replicate 'a' :: Either (Sum Int) (Sum Int) -> String:

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)

Ich denke jedoch, dass es der Fall sein könnte, dass für nicht kommutative Monoide die einzig mögliche Implementierung ist const mempty(für die ich noch keinen Beweis habe).