Le seul `FlippyFloppyMorphism` est-il` const mempty`?

Question

Dans Haskell, nous avons le fait intéressant que tout constructeur de type f :: * -> *qui est simultanément a Functoret a Contravariantest fantôme dans son paramètre de type:

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

Une autre façon de dire cela est que chaque constructeur de type qui est simultanément un Functors et un Contravariantest naturellement isomorphe à Const x, pour certains x.

Cela implique que la "seule" façon (jusqu'à l'isomorphisme) d'instancier la classe:

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

pour qu'il obéisse aux lois des foncteurs:

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)

est:

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

à- dire modulo newtypes, const id.

J'ai du mal à comprendre pourquoi c'est la seule fonction de son type qui satisfait les contraintes, bien que je puisse en quelque sorte comprendre divers arguments informels impliquant absurd :: Void -> a/ discard :: a -> ()quant à la raison pour laquelle l'existence d'une telle carte implique que le foncteur "est fantôme" dans son type paramètre.

Pour mieux le comprendre, j'ai essayé de simplifier le problème. Au lieu de réfléchir FlippyFloppyFunctor, réfléchissons à:

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

avec des lois analogues:

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)

En supposant que aet que ce b sont des monoïdes non commutatifs , est-il toujours vrai que la seule implémentation légale de FlippyFloppyMorphismest const mempty? Est - il encore possible d'expliquer pourquoi le morphisme doit être « fantôme » dans les monoïdes d'entrée, sans avoir Voidou de ()se référer à?

Answer 1

Il me semble que la réponse dans le cas général est «non», car les monoïdes peuvent être commutatifs.

Si le monoïde est commutatif, alors Dual aest le même monoïde que a, et Either a aest le même que a, et par conséquent nous dégénérons juste pour demander si ffmorphest le seul homomorphisme monoïde a -> b. La réponse est non".

Par exemple, pour le monoïde commutatif d'addition, on a replicate 'a' :: Either (Sum Int) (Sum Int) -> String, où:

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)

Cependant, je pense qu'il pourrait être le cas que pour les monoïdes _non_commutatifs, la seule implémentation possible est const mempty(pour laquelle je n'ai toujours pas de preuve).