¿Es el único "FlippyFloppyMorphism" "const mempty"?

Question

En Haskell, tenemos el hecho interesante de que cualquier tipo de constructor f :: * -> *que es al mismo tiempo una Functory una Contravariantes fantasma en su parámetro de tipo:

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

Otra forma de decir esto es que cada constructor de tipos que es simultáneamente una Functors y una Contravariantes naturalmente isomorfo a Const x, para algunos x.

Esto implica que la "única" forma (hasta el isomorfismo) de instanciar la clase:

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

para que obedezca las leyes del 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)

es:

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

es decir modulo Newtypes, const id.

Encuentro difícil entender por qué esta es la única función de su tipo que satisface las restricciones, aunque puedo entender varios argumentos informales que involucran absurd :: Void -> a/ discard :: a -> ()sobre por qué la existencia de tal mapa implica que el functor "es fantasma" en su tipo parámetro.

Para entenderlo mejor, intenté simplificar el problema. En lugar de pensar FlippyFloppyFunctor, pensemos en:

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

con leyes 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)

Suponiendo que ay b son monoides no conmutativos , ¿sigue siendo cierto que la única implementación legal de FlippyFloppyMorphismes const mempty? ¿Todavía es posible explicar por qué el morfismo debe ser "fantasma" en los monoides de entrada, sin tener a Voido a ()para referirse?

Answer 1

Me parece que la respuesta en el caso general es "no", porque los monoides pueden ser conmutativos.

Si el monoide es conmutativo, entonces Dual aes el mismo monoide que a, y Either a aes el mismo que a, y por lo tanto degeneramos en preguntarnos si ffmorphes el único homomorfismo de monoide a -> b. La respuesta es no".

Por ejemplo, para el monoide conmutativo de suma, tenemos replicate 'a' :: Either (Sum Int) (Sum Int) -> String, donde:

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)

Sin embargo, creo que podría ser el caso de que para los monoides _non_conmutative, la única implementación posible es const mempty(de la que todavía no tengo una prueba).