----------
Monads!
----------
Eugenio Moggi

Teorema:
Para qualquer adjunção F -| G com unidade eta, a composta F;G é um monad
Para qualquer Monad M : C -> C,
existem:
categoria D
funtor F : C -> D
funtor G : D -> C
tais que M = F;G
e F -| G

uma ideia para a prova do segundo é quando D
é a chamada "categoria de Kleisli" do Monad M
mesmos objetos que C
mesmas setas
mesmos domínios
contradomínio muda: na categoria de Kleisli, uma seta é de tipo f : a -> b
se na original C ela era f : a -> M b

"problema": composta na categoria de Kleisli!
se temos (na cat. Kleisli)
f : a -> b, g : b -> c
precisamos que f;g : a -> c
em C, isso é
f : a -> M b, g : b -> M c
então em C elas não podem ser compostas!!
quero, em C, uma operação que eu possa "aplicar" a f e g, e me dê uma seta a -> M c
(>=>) :: (a -> M b) -> (b -> M c) -> (a -> M c)
em C

outro problema: identidades!
quero id : a -> a na categoria de Kleisli
ou seja, quero em C:
"id" : a -> M a (pure!!!)

para Monads, "pure" se chama "return"


===========
Definição 1:
um Monad é um Applicative que implementa (>=>) "fish"

em direção a uma outra definição:
se eu quisesse "implementar" o (>=>), o que eu gostaria de ter:

assumindo que M é Functor, Applicative

f :: a -> M b, g :: b -> M c
f >=> g :: a -> M c
(f >=> g) val_a = join (g <$> (f val_a))
onde join :: M (M c) -> M c

===========
Def 2: um Monad é um Applicative que implementa join

===========
Def 3: um Monad é um Applicative que implementa (>>=) "bind"
(>>=) :: m a -> (a -> m b) -> m b

enc_x :: m a
g :: a -> m b
enc_x >>= g = join (g <$> enc_x)

Exercícios: escrever cada um dentre >=>, join, >>= em função de cada um dos outros (mais return)