É o único `FlippyFloppyMorphism`` const mempty`?

Question

Em Haskell, temos o fato interessante de que qualquer construtor de tipo f :: * -> *que seja simultaneamente a Functore a Contravarianté fantasma em seu parâmetro de tipo:

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

Outra maneira de colocar isso é que todo construtor de tipo que é simultaneamente a se Functora Contravarianté naturalmente isomórfico a Const x, para alguns x.

Isso implica que a "única" maneira (até o isomorfismo) de instanciar a classe:

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

para que obedeça às leis do functor:

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)

é:

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

ou seja, módulo newtypes const id,.

Acho difícil entender por que esta é a única função de seu tipo que satisfaz as restrições, embora eu possa entender vários argumentos informais envolvendo absurd :: Void -> a/ discard :: a -> ()sobre por que a existência de tal mapa implica que o functor "é fantasma" em seu tipo parâmetro.

Para entender melhor, tentei simplificar o problema. Em vez de pensar FlippyFloppyFunctor, vamos pensar sobre:

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

com leis análogas:

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)

Supondo que ae b sejam monóides não comutativos , ainda é verdade que a única implementação legal de FlippyFloppyMorphismé const mempty? Ainda é possível explicar por que o morfismo deve ser "fantasma" nos monoides de entrada, sem ter a Voidou a ()para se referir?

Answer 1

Parece-me que a resposta no caso geral é "não", porque os monóides podem ser comutativos.

Se o monóide é comutativo, então Dual aé o mesmo monóide que a, e Either a aé o mesmo que a, e portanto degeneramos e perguntamos se ffmorphé o único homomorfismo monóide a -> b. A resposta é não".

Por exemplo, para o monóide comutativo de adição, temos replicate 'a' :: Either (Sum Int) (Sum Int) -> String, onde:

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)

No entanto, acho que pode ser o caso de que para _non_commutative monoides, a única implementação possível é const mempty(para a qual ainda não tenho uma prova).