Uma mônada é apenas um monoide na categoria de endofunctores, qual'é o problema?

Quem disse primeiro o seguinte?

Uma mônada é apenas uma monoide no categoria dos endofunctores, o que's o problema?

E, numa nota menos importante, isto é verdade e se assim for, poderia dar uma explicação (esperançosamente uma que possa ser compreendida por alguém que não'não tenha muita experiência de Haskell)?

Solução

Essa frase em particular é de James Iry, do seu altamente divertido Breve, Incompleto e Principalmente Errado História das Linguagens de Programação, no qual ele a atribui ficcionalmente a Philip Wadler.

A citação original é de Saunders Mac Lane em Categorias para o Matemático de Trabalho, um dos textos fundamentais da Teoria da Categoria. Aqui está no contexto, que é provavelmente o melhor lugar para aprender exatamente o que significa.

Mas, eu vou dar uma facada. A frase original é esta:

Ao todo, uma mônada em X é apenas um monóide na categoria de endofunctores de X, com produto × substituído por composição de endofunctores e unidade definida pelo endofunctor de identidade.

X aqui é uma categoria. Endofunctores são functores de uma categoria para si próprios (que normalmente é todos 'functores' no que diz respeito a programadores funcionais, uma vez que na sua maioria lidam apenas com uma categoria; a categoria dos tipos - mas eu divago). Mas você poderia imaginar outra categoria que é a categoria de "endofunctores em *X**". Esta é uma categoria na qual os objetos são endofunctores e os morfismos são transformações naturais.

E desses endofunctores, alguns deles podem ser mônadas. Quais delas são mônadas? Exactamente as que são monoidais num sentido particular. Em vez de escrever o mapeamento exato das mônadas para monoides (já que a Mac Lane faz isso muito melhor do que eu poderia esperar), vou apenas colocar suas respectivas definições lado a lado e deixar você comparar:

Um monoide é...

Um conjunto, *S**

  • Uma operação, *- : S × S → S**
  • Um elemento de S, *e : 1 → S**

... satisfazendo estas leis:

(a - b) - c = a - (b - c), para todos a, b e c em S e - a = a - a - e = a, para todos a em S

Uma mônada é...

*Um endofunctor, *T : X → X** (em Haskell, um construtor do tipo * -> * com uma instância Functor)

  • Uma transformação natural, *μ : T × T → T**, onde × significa composição funerária (μ é conhecido como `join em Haskell)
  • Uma transformação natural, η : I → T, onde I é o endofunctor de identidade em X (η é conhecido como return em Haskell)

... satisfazendo estas leis:

  • μ ∘ Tμ = μ ∘ μT
  • μ ∘ Tη = μ ∘ ηT = 1 (a transformação natural da identidade)

Com um pouco de caolho você pode ver que ambas as definições são instâncias do mesmo conceito abstrato.

Comentários (46)

Intuitivamente, eu acho que o que o vocabulário de matemática chique está dizendo é isso:

Monoid

A **monoid*** é um conjunto de objectos e um método de os combinar. Monoides bem conhecidos são:

  • números que você pode adicionar
  • listas que você pode concatenar
  • conjuntos que você pode unir

Há também exemplos mais complexos.

Além disso, tudo o monóide tem uma identidade, que é aquele elemento "no-op" que não tem efeito quando você o combina com outra coisa:

  • 0 + 7 == 7 + 0 == 7
  • [] ++ [1,2,3] == [1,2,3] ++ [] == [1,2,3]
  • {} union {apple} ==* {apple} union {} ==* {apple}

Finalmente, um monoide deve ser **associativo***. (você pode reduzir uma longa seqüência de combinações como quiser, desde que não altere a ordem da esquerda para a direita dos objetos) A adição é OK ((5+3)+1 == 5+(3+1)), mas a subtração não é ((5-3)-1 != 5-(3-1)).

Mônada

Agora, vamos considerar um tipo especial de conjunto e uma forma especial de combinar objectos.

Objetos

Suponha que o seu conjunto contenha objetos de um tipo especial: **funções***. E estas funções têm uma assinatura interessante: Não transportam números para números ou cordas para cordas. Em vez disso, cada função transporta um número para uma lista de números em um processo de dois passos.

  1. Calcule 0 ou mais resultados
  2. Combine esses resultados com uma única resposta de alguma forma.

Exemplos:

  • 1 -> [1] (basta embrulhar a entrada)
  • 1 -> [] (descarte a entrada, envolva o nada em uma lista)
  • 1 -> [2] (adicionar 1 à entrada, e embrulhar o resultado)
  • 3 -> [4, 6] (adicionar 1 à entrada e multiplicar a entrada por 2, e embrulhar os resultados múltiplos)

Combinando Objetos

Além disso, a nossa forma de combinar funções é especial. Uma forma simples de combinar funções é a composição: Vamos pegar nossos exemplos acima, e compor cada função com ela mesma:

  • 1 -> [1] -> [[1]] (embrulhe a entrada, duas vezes)
  • 1 -> [] -> [] (descartar a entrada, embrulhar o nada em uma lista, duas vezes)
  • 1 -> [2] -> [ UH-OH! ] (não podemos "adicionar 1" a uma lista!")
  • 3 -> [4, 6] -> [ UH-OH! ] (não podemos "adicionar 1" a uma lista!)

Sem entrar muito na teoria do tipo, a questão é que você pode combinar dois inteiros para obter um inteiro, mas você nem sempre pode compor duas funções e obter uma função do mesmo tipo. (Funções com tipo a -> a irão compor, mas a-> [a] não irá).

Então, vamos definir uma maneira diferente de combinar funções. Quando combinamos duas destas funções, não queremos "embrulhar" os resultados.

Aqui está o que nós fazemos. Quando queremos combinar duas funções F e G, nós seguimos este processo (chamado coberta):

  1. Calcule os "resultados" de F, mas não os combine.
    1. Calcule os resultados da aplicação de G a cada um dos resultados de F separadamente, produzindo uma coleção de resultados.
  2. Aplainar a colecção de 2 níveis e combinar todos os resultados.

Voltando aos nossos exemplos, vamos combinar (vincular) uma função com ela mesma usando esta nova forma de funções "vinculadas":

  • 1 -> [1] -> [1] (embrulhe a entrada, duas vezes)
  • 1 -> [] -> [] (descartar a entrada, embrulhar o nada em uma lista, duas vezes)
  • 1 -> [2] -> [3] (adicionar 1, depois adicionar 1 novamente, e embrulhar o resultado).
  • 3 -> [4,6] -> [5,8,7,12] (adicione 1 à entrada, e também multiplique a entrada por 2, mantendo ambos os resultados, depois faça tudo novamente a ambos os resultados, e depois embrulhe os resultados finais em uma lista).

Esta forma mais sofisticada de combinar funções é associativa (seguindo a forma como a composição da função é associativa quando você não está fazendo o material de embrulho chique).

Amarrar tudo junto,

  • uma mônada é uma estrutura que define uma forma de combinar (os resultados de) funções,
  • analogamente a como um monoide é uma estrutura que define uma forma de combinar objetos,
  • onde o método de combinação é associativo, e onde há um 'No-op' especial que pode ser combinado com qualquer something para resultar em something* unchanged.

Notas

Há muitas maneiras de "embrulhar" os resultados. Você pode fazer uma lista, ou um conjunto, ou descartar todos, exceto o primeiro resultado, observando se não houver resultados, anexar um sidecar de estado, imprimir uma mensagem de log, etc, etc.

Eu joguei um pouco solto com as definições na esperança de transmitir a idéia essencial de forma intuitiva.

Simplifiquei um pouco as coisas insistindo que a nossa mônada opera em funções do tipo a -> [a]. Na verdade, as mônadas funcionam em funções do tipo a -> m b, mas a generalização é uma espécie de detalhe técnico que não é o principal discernimento.

Comentários (6)

Primeiro, as extensões e bibliotecas que vamos usar:

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

Destes, 'RankNTypes' é o único que é absolutamente essencial para os abaixo. Uma vez escrevi uma explicação de 'RankNTypes' que algumas pessoas parecem ter achado útil]1, então eu vou me referir a isso.

Citando a excelente resposta de Tom Crockett, nós temos:

Uma mônada é...

Um endofunctor, *T : X -> X**

  • Uma transformação natural, *μ : T × T -> T***, onde × significa composição funerária Uma transformação natural, η : I -> T**, onde I é o endofunctor de identidade em X*

...satisfazendo estas leis:

  • μ(μ(T × T) × T)) = μ(T × μ(T × T))
  • μ(η(T)) = T = μ(T(η))

Como é que traduzimos isto para o código Haskell? Bem, vamos começar com a noção de uma transformação natural:

-- | A natural transformations between two 'Functor' instances.  Law:
--
-- > fmap f . eta g == eta g . fmap f
--
-- Neat fact: the type system actually guarantees this law.
--
newtype f :-> g =
    Natural { eta :: forall x. f x -> g x }

Um tipo de formulário f :-> g é análogo a um tipo de função, mas em vez de pensar nele como uma função entre dois tipos (do tipo *), pense nele como um morfismo entre dois funcionadores (cada um do tipo * -> *). Exemplos:

listToMaybe :: [] :-> Maybe
listToMaybe = Natural go
    where go [] = Nothing
          go (x:_) = Just x

maybeToList :: Maybe :-> []
maybeToList = Natural go
    where go Nothing = []
          go (Just x) = [x]

reverse' :: [] :-> []
reverse' = Natural reverse

Basicamente, em Haskell, as transformações naturais são funções de algum tipo f x para outro tipo g x, de modo que a variável do tipo x é "inacessível" para o chamador. Então, por exemplo, sort :: Ord a => [a] -> [a] não pode ser feita uma transformação natural, porque é "picuinhas" sobre quais tipos podemos instanciar para a. Uma forma intuitiva que eu costumo usar para pensar nisso é a seguinte:

  • Um functor é uma forma de operar no content de algo sem tocar na estrutura.
  • Uma transformação natural é uma forma de operar na estrutura de algo sem tocar ou olhar para o contente.

Agora, com isso fora do caminho, vamos abordar as cláusulas da definição.

A primeira cláusula é "um endofunctor, *T : X -> X**". Bem, todo Functor em Haskell é um endofunctor no que as pessoas chamam de "a categoria Hask", cujos objetos são do tipo Haskell (do tipo *) e cujos morfismos são funções Haskell. Isto soa como uma afirmação complicada, mas na verdade é muito trivial. Tudo o que isso significa é que um Functor f :: * -> * dá-lhe os meios para construir um tipo f a :: * `` para qualquera :: *e uma funçãofmap f :: f a -> f bde qualquerf :: a -> b`, e que estes obedecem às leis funerárias.

Segunda cláusula: o functor Identidade em Haskell (que vem com a Plataforma, então você pode simplesmente importá-la) é definido desta forma:

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity where
    fmap f (Identity a) = Identity (f a)

Então a transformação natural *η : I -> T** da definição de Tom Crockett pode ser escrita desta forma para qualquer instância Monad t:

return' :: Monad t => Identity :-> t
return' = Natural (return . runIdentity)

Terceira cláusula: A composição de dois funtores em Haskell pode ser definida desta forma (que também vem com a Plataforma):

newtype Compose f g a = Compose { getCompose :: f (g a) }

-- | The composition of two 'Functor's is also a 'Functor'.
instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose fga) = Compose (fmap (fmap f) fga)

Então a transformação natural *μ : T × T -> T** da definição do Tom Crockett pode ser escrita assim:

join' :: Monad t => Compose t t :-> t
join' = Natural (join . getCompose)

A afirmação de que este é um monóide na categoria de endofunctores significa então que "Compor" (parcialmente aplicado apenas aos seus dois primeiros parâmetros) é associativo, e que "Identidade" é o seu elemento de identidade. Isto é, que os seguintes isomorfismos são válidos:

  • Compose f (Compose g h) ~= Compose (Compose f g) h
  • Compose f Identidade ~= f
  • Compor Identidade g ~= g

Estes são muito fáceis de provar porque "Compor" e "Identidade" são ambos definidos como "novo tipo", e os Relatórios Haskell definem a semântica do "novo tipo" como um isomorfismo entre o tipo que está sendo definido e o tipo de argumento para o construtor de dados do "novo tipo". Então, por exemplo, vamos provar Compose f Identity ~= f:

Compose f Identity a
    ~= f (Identity a)                 -- newtype Compose f g a = Compose (f (g a))
    ~= f a                            -- newtype Identity a = Identity a
Q.E.D.
Comentários (4)