programmers for haskell category-theory

for - ¿Cuáles son los pares de funtores adjuntos correspondientes a las mónadas comunes en Haskell?



category theory for programmers (3)

En la teoría de categorías, una mónada puede construirse a partir de dos funtores adjuntos. En particular, si C y D son categorías y F: C -> D y G: D -> C son funtores adjuntos, en el sentido de que hay una biyección

hom (FX, Y) = hom (X, GY)

para cada X en C e Y en D, entonces la composición G o F: C -> C es una mónada.

Uno de esos pares de funtores adjuntos se puede dar fijando un tipo b y tomando F y G para ser

data F b a = F (a,b) data G b a = G (b -> a) instance Functor (F b) where fmap f (F (a,b)) = F (f a, b) instance Functor (G b) where fmap f (G g) = G (f . g)

y la biyección entre hom-sets se da (modulo constructors) currying:

iso1 :: (F b a -> c) -> a -> G b c iso1 f = /a -> G $ /b -> f (F (a,b)) iso2 :: (a -> G b c) -> F b a -> c iso2 g = /(F (a,b)) -> let (G g'') = g a in g'' b

en cuyo caso la mónada correspondiente es

data M b a = M { unM :: b -> (a,b) } instance Monad (M b) where return a = M (/b -> (a,b)) (M f) >>= g = M (/r -> let (a,r'') = f r in unM (g r'') a)

No sé cuál debería ser el nombre de esta mónada, excepto que parece ser algo así como una mónada de lector que lleva consigo una información sobreescrita ( edit: dbaupp señala en los comentarios que esta es la mónada del State .)

Entonces, la mónada de State puede "descomponerse" como el par de funtores adjuntos F y G , y podríamos escribir

State = G . F

Hasta aquí todo bien.

Ahora estoy tratando de descubrir cómo descomponer otras mónadas comunes en pares de funtores adjuntos, por ejemplo, Maybe , [] , Reader , Writer , Cont . Pero no puedo entender cuáles son los pares de funtores adjuntos que podemos ". descomponerlos en "are".

El único caso simple parece ser la mónada de Identity , que puede descomponerse en cualquier par de funtores F y G modo que F sea ​​inversa a G (en particular, podría tomar F = Identity y G = Identity ).

¿Alguien puede arrojar algo de luz?


Como observa, cada par de funtores adjuntos da lugar a una mónada. Lo contrario también se sostiene: cada mónada surge de esa manera. De hecho, lo hace de dos maneras canónicas. Una es la construcción Kleisli que describe Petr; el otro es la construcción de Eilenberg-Moore. De hecho, Kleisli es la inicial y EM el terminal, en una categoría adecuada de pares de funtores adjuntos. Fueron descubiertos de forma independiente en 1965. Si desea los detalles, le recomiendo los videos de Catsters .


Lo que estás buscando es la categoría Kleisli . Fue desarrollado originalmente para mostrar que cada mónada se puede construir a partir de dos funtores adjuntos.

El problema es que Haskell Functor no es un functor genérico, es un endo-functor en la categoría Haskell. Entonces, necesitamos algo diferente (AFAIK) para representar funtores entre otras categorías:

{-# LANGUAGE FunctionalDependencies, KindSignatures #-} import Control.Arrow import Control.Category hiding ((.)) import qualified Control.Category as C import Control.Monad class (Category c, Category d) => CFunctor f c d | f -> c d where cfmap :: c a b -> d (f a) (f b)

Tenga en cuenta que si tomamos -> para c y d obtenemos un endo-functor de la categoría Haskell, que es solo el tipo de fmap :

cfmap :: (a -> b) -> (f a -> f b)

Ahora tenemos una clase de tipo explícita que representa funtores entre dos categorías dadas c y d y podemos expresar los dos funtores adjuntos para una mónada determinada. El izquierdo mapea un objeto a a solo a y mapea un morfismo f a (return .) f :

-- m is phantom, hence the explicit kind is required newtype LeftAdj (m :: * -> *) a = LeftAdj { unLeftAdj :: a } instance Monad m => CFunctor (LeftAdj m) (->) (Kleisli m) where cfmap f = Kleisli $ liftM LeftAdj . return . f . unLeftAdj -- we could also express it as liftM LeftAdj . (return .) f . unLeftAdj

El derecho asigna un objeto a al objeto ma y mapea un morfismo g para join . liftM g join . liftM g , o equivalentemente a (=<<) g :

newtype RightAdj m a = RightAdj { unRightAdj :: m a } instance Monad m => CFunctor (RightAdj m) (Kleisli m) (->) where cfmap (Kleisli g) = RightAdj . join . liftM g . unRightAdj -- this can be shortened as RightAdj . (=<<) g . unRightAdj

(Si alguien conoce una mejor manera de expresar esto en Haskell, hágamelo saber).


  • Maybe proviene del functor gratuito en la categoría de conjuntos puntiagudos y el functor olvidadizo
  • [] proviene del functor gratuito en la categoría de monoides y del functor olvidadizo

Pero ninguna de estas categorías son subcategorías de Hask.