Categoria das Mônadas

Esse post é baseado no livro Teoria das Categorias para Programadores, de Bartosz Milewski.

1 Categoria Monad

Considere a expressão algébrica \(x^2 + 2x + 1\) que, computacionalmente, podemos representar como uma árvore de expressão:

Denotando a variável \(x\) como um objeto a de uma categoria, temos que nossa árvore de expressão é um objeto m a, sendo m um endofunctor contendo valores do tipo a. Uma operação comum em expressões algébricas é a substituição de variáveis, seja para simplificação, avaliação ou transformação. Podemos substituir toda ocorrência de \(x\) da árvore acima por \(y - 1\), gerando a expressão \((y-1)^2 + 2(y-1) + 1\) e a árvore:

Se \(y\) é um objeto b de nossa categoria, temos que a expressão \(y - 1\) é um tipo m b. Nossa transformação pode ser representada por:

,#+begin_src haskell subst :: m a -> (a -> m b) -> m b #+end_src

que é o operador bind que definimos para Monads. Portanto, uma outra forma de pensar em Monads é na manipulação de expressões algébricas via substituição.

Na matemática um Monad é representado pela letra \(T\), que representa um endofunctor, a operação join é representada pela transformação natural \(\mu\) e o return por \(\eta\):

\(\mu :: T^2 \rightarrow T\)

\(\eta :: I \rightarrow T\)

Que, aplicando um objeto a são equivalentes a:

\(\mu_a :: T (T a) \rightarrow T a\)

\(\eta_a :: a \rightarrow T a\)

Com isso, se tivermos os morfismos \(f :: a \rightarrow T b\) e \(g :: b \rightarrow T c\), a composição e definida por:

\(g \circ_T f = \mu_c \circ (T g) \circ f\)

que em Haskell se traduziria (lembrando que um Functor funciona em morfismos) em:

join (fmap g (f a))

Em álgebra, isso representa a composição de duas substituições.

Dissecando um pouco mais as definições de \(\mu, \eta\), percebemos que \(\mu\) age como a multiplicação de dois endofunctors enquanto \(\eta\) funciona como uma identidade na composição de Functors:

mu :: (m, m) -> m
=
mu :: m -> m -> m

eta :: () -> m
=
eta :: m

Essas duas definições são isomórficas com as definições de mappend e mempty da classe Monoid. Vamos verificar se as propriedades de um Monoid são garantidas:

mu (x, mu (y, z)) = mu (mu (x, y), z)

Para um tipo produto temos a definição de Bifunctors para mapear as funções, com isso temos:

(mu . bimap id mu) (x, (y,z)) = (mu . bimap mu id) ((x,y),z)

Para transformar essa equação em point-free, temos que aplicar uma transformação natural alpha para rearranjar os tipos produtos:

alpha :: (a, (b, c)) -> ((a, b), c)
alpha (x, (y,z)) = ((x,y), z)

com isso temos:

(mu . bimap id mu) . alpha = (mu . bimap mu id)

A propriedade de identidade é fácil de verificar:

mu (eta (), x) = x
mu (x, eta ()) = x

que se tornam:

(mu . bimap eta id) ((), x) = lambda ((), x)
(mu . bimap id eta) (x, ()) = rho (x, ())

Podemos então generalizar uma Categoria Monoidal como toda categoria que possui um Bifunctor, chamado de produto tensorial \(otimes\) e um objeto terminal \(i\), denominado unit que satisfaçam as propriedades dos Monoids.

Com essas definições podemos chegar na definição de Monads em que temos o endofunctor \(T\), o Functor identidade \(I\), a composição de Functors \(\circ\) e duas transformações naturais:

mu  :: T . T -> T
eta :: I -> T

Ou seja, um Monad é um Monoid na categoria dos endofunctors (Saunders Mac Lane).

2 Monads de Adjuntos

Relembrando a definição de dois Functors adjuntos, \(L, R\), como um par de Functors em que L :: D -> C e R :: C -> D de tal forma que a composição deles forma o Functor identidade. Eles são equipados com dois morfismos:

unit :: I -> R . L
counit :: L . R -> I

Podemos verificar que a composição R . L forma um Monad, sendo a definição de unit equivalente ao return. O join pode ser construido partindo da definição de counit:

join :: R . L . R . L -> R . L
=
join :: R . (L . R) . L -> R . L
join = R . counit . L

Como Functos adjuntos geralmente envolvem duas categorias distintas, é difícil encontrar exemplos em Haskell. Repetindo o exemplo dado nesse tópico, podemos fazer com que L = (,s) = Writer s e R = (s->) = Reader s. A composição R . L dos dois define Reader s (Writer s a) que é a definição do Monad State.

Para esse Monad, as definições de unit :: a -> Reader s (Writer s a) e counit :: Writer s (Reader s a) -> a podem ser dadas por:

unit :: a -> s -> (a, s)
unit x = \s -> (x, s)

counit :: (s -> a, s) -> a
counit (f, s) = f s

Reparem que a definição de unit é equivalente ao return de nosso Monad e counit equivale a runState seguido de uncurry. Como definimos o join?

join :: State s (State s a) -> State s a
-- = R . counit . L
join ssa = State (uncurry runState . runState ssa)

3 Categoria dos Comonads

Da mesma forma podemos pensar em Comonads como uma categoria de endofunctors, porém o dual do Monoid, o Comonoid. Nessa categoria temos dois morfismos:

eps :: T -> I        -- extract / counit
delta :: T -> (T, T) -- duplicate

Analogamente, percebemos que eps representa o counit, com T = L.R e, utilizando eta :: I -> R.L podemos fazer delta = L . eta . R = L . R . L . R = (T, T). Com isso podemos definir um Comonoid como:

class Comonoid m where
  split :: m -> (m, m)
  destroy :: m -> ()
  destroy _ = ()

Dessa forma, um Comonad é um Comonoid da categoria dos endofunctors..

4 Referências

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/