haskell - quiere - ¿La mónada libre siempre existe?

neo monadología

Question

Sabemos por la teoría de categorías que no todos los endofunctors en Set admiten una mónada gratuita. El contraejemplo canónico es el functor powerset.

Pero Haskell puede convertir cualquier functor en una mónada gratuita.

data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Monad (Free f) where
  return = Pure
  Pure a >>= f = f a
  Free m >>= f = Free ((>>= f) <$> m)

¿Qué hace que esta construcción funcione para cualquier functor de Haskell pero se descompone en Set ?

Answer 1

Está claro que esta respuesta es incorrecta . Lo dejo aquí para preservar una discusión valiosa en los comentarios hasta que alguien formule una respuesta correcta .

Considere la potencia establecida en Set . Si tenemos una función f : S -> T , podemos formar f'' : PS S -> PS T con f'' X = f [X] . Buen functor covariante (creo). También podríamos formar f'''' X = f^(-1) [X] , un simpático functor contravariante (creo).

Veamos el "conjunto de poder" en Haskell:

newtype PS t = PS (t -> Bool)

Esto no es un Functor , sino solo un Contravariant :

instance Contravariant PS where
  contramap f (PS g) = PS (g . f)

Reconocemos esto porque t está en posición negativa. A diferencia de Set , no podemos acceder a los "elementos" de las funciones características que componen el conjunto de potencias, por lo que el funtor covariante no está disponible.

Conjeturaría, por lo tanto, que la razón por la que Haskell admite una mónada libre para cada functor covariante es que excluye los funtores covariantes que causan problemas para Set .

Answer 2

Yo (más bien) tengo la sospecha de que esta no es exactamente una definición. Digamos, esta fórmula recursiva especifica un punto fijo; ahora, ¿cómo sabemos que existe este punto fijo? ¿Cómo sabemos que solo hay un punto fijo? Y más aún, ¿cómo define Free m >>= algo, excepto tal vez en el caso en que supongamos que solo tenemos secuencias finitas de aplicaciones de Free ?