La definizione "Monade sono solo monoidi nella categoria dei endofunzionisti", che sebbene sia vero è un brutto punto di partenza. Proviene da uno blog post che era in gran parte inteso per essere uno scherzo. Ma se sei interessato alla corrispondenza può essere dimostrato in Haskell:
La descrizione del laico di una categoria è una raccolta astratta di oggetti e morfismi tra gli oggetti. I mapping tra categorie sono chiamati functors e mappano oggetti e morfismi ai morfismi in modo associativo e preservano le identità. Un endofunctor è un funtore di una categoria a se stesso.
{-# LANGUAGE MultiParamTypeClasses,
ConstraintKinds,
FlexibleInstances,
FlexibleContexts #-}
class Category c where
id :: c x x
(.) :: c y z -> c x y -> c x z
class (Category c, Category d) => Functor c d t where
fmap :: c a b -> d (t a) (t b)
type Endofunctor c f = Functor c c f
mappature tra funtori che soddisfano il cosiddetto naturality conditions sono chiamati trasformazioni naturali. In Haskell queste sono funzioni polimorfiche di tipo: (Functor f, Functor g) => forall a. f a -> g a.
Un monade su una categoria C è tre cose (T,η,μ), T è endofunctor e 1 è il funtore identità su C. Mu e eta sono due trasformazioni fisiche che soddisfano un triangle identity e un associatività identità, e sono definiti come:
In Haskell μ è join e η è return
return :: Monad m => a -> m ajoin :: Monad m => m (m a) -> m a
Una definizione categoriale della Monade in Haskell potrebbe scrivere:
class (Endofunctor c t) => Monad c t where
eta :: c a (t a)
mu :: c (t (t a)) (t a)
L'operatore si legano può essere derivata da questi.
(>>=) :: (Monad c t) => c a (t b) -> c (t a) (t b)
(>>=) f = mu . fmap f
Si tratta di una definizione completa, ma in modo equivalente si può anche dimostrare che le leggi Monade possono essere espresse come leggi monoid con una categoria funtore. Possiamo costruire questa categoria di functor che è una categoria con oggetti come funtori (cioè mappature tra categorie) e trasformazioni naturali (cioè mappature tra funtori) come morfismi. In una categoria di endofosfori tutti i funtori sono funtori tra la stessa categoria.
newtype CatFunctor c t a b = CatFunctor (c (t a) (t b))
possiamo mostrare questo dà luogo ad una categoria con composizione funtore la composizione morfismo:
-- Note needs UndecidableInstances to typecheck
instance (Endofunctor c t) => Category (CatFunctor c t) where
id = CatFunctor id
(CatFunctor g) . (CatFunctor f) = CatFunctor (g . f)
Il monoide ha la solita definizione:
class Monoid m where
unit :: m
mult :: m -> m -> m
un monoide su una categoria di i funtori hanno una trasformazione naturale come identità a e un'operazione di moltiplicazione che combina le trasformazioni naturali. La composizione di Kleisli può essere definita per soddisfare la legge sulla moltiplicazione.
(<=<) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z)
f <=< g = mu . fmap f . g
E così avete "Monadi sono monoidi solo nella categoria endofunctors", che è solo una versione "pointfree" della normale definizione di monadi da endofunctors e (mu, ETA).
instance (Monad c t) => Monoid (c a (t a)) where
unit = eta
mult = (<=<)
Con un po 'di sostituzione si può dimostrare che le proprietà di monoidali (<=<) sono dichiarazione equivalente del triangolo e associatività diagrammi per le trasformazioni naturali della monade.
f <=< unit == f
unit <=< f == f
f <=< (g <=< h) == (f <=< g) <=< h
Se siete interessati a diagrammatic representations ho scritto un po 'su di loro che rappresentano con i diagrammi di stringa.
.
aah, Monad è endofuctor, come mi sono perso. Adesso è chiaro, grazie. –