Esse post é baseado no livro Teoria das Categorias para Programadores, de Bartosz Milewski.
Para verificar se dois tipos A, B
são isomórficos, basta definirmos
duas funções f :: A -> B, g :: B -> A
de tal forma que f . g = id
e
g . f = id
. Por exemplo, podemos verificar que (a, b)
e (b, a)
são
isomórficos pois:
swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)
E temos que swap . swap = id
é válido para os dois lados.
Como podemos definir o isomorfismo entre duas categorias
e
lembrando que o Functor identidade é dado por:
data Identity a = Identity a
instance Functor Identity where
fmap f (Identity x) = Identity (f x)
Para provar que duas categorias são isomórficas, precisamos definir transformações naturais entre a composição dos Functors e o Functor Identidade:
eta :: Id -> (R.L)
eta' :: (R.L) -> Id
eps :: (L.R) -> Ic
eps' :: Ic -> (L.R)
garantindo que eta . eta' = R.L
, eta' . eta = Id
e
eps . eps' = Ic
, eps' . eps = L.R
.
Dizemos que dois Functors R, L
são adjuntos se eles possuem as
transformações naturais eta, eps
, mas sem a necessidade de existir
eta', eps'
.
O Functor L
é denominado adjunto esquerdo (left adjunct), R
é o
adjunto direito (right adjunct), eta
é chamado de unit
e eps
de
counit
. Denotamos
A função eta
pega um objeto de D
e faz um passeio entre as
categorias C, D
utilizando os Functors R . L
, retornando em outro
objeto de D
. Já o counit
faz:
A função eps
indica como chegar em c'
partindo de c
seguindo o
caminho L . R
.
Em outras palavras, o unit
(também chamado de return
e pure
em
outros contextos) permite introduzir um container ou Functor R.L
em
todo tipo d
. Por outro lado, o counit
(em algumas linguagens
conhecido como extract
) permite retirar um objeto de um container ou
Functor:
-- F = R . L
-- G = L . R
unit :: d -> F d
counit :: G c -> c
A classe de Functors adjuntos é definido como:
class (Functor f, Representable y) =>
Adjunction f u | f -> u, u -> f where
unit :: a -> u (f a)
counit :: f (u a) -> a
A condição f -> u, u -> f
é uma dependência funcional e implica que
só pode existir uma única instância para f
na esquerda e para u
a
direita. Ou seja, se eu defino Adjunction [] (Reader a)
, não posso
definir Adjunction Maybe (Reader a)
nem Adjunction [] Maybe
. Junto
dessas duas funções também podemos definir essa classe através de
leftAdjunction
e rightAdjunction
:
class (Functor f, Representable y) =>
Adjunction f u | f -> u, u -> f where
leftAdjunct :: (f a -> b) -> a -> u b
rightAdjunct :: (a -> u b) -> f a -> b
E elas se relacionam da seguinte forma:
unit = leftAdjunct id
counit = rightAdjunct id
leftAdjunct = fmap g . unit
rightAdjunct = counit . fmap g
Existem poucos Functors pertencentes a
Um exemplo de Functors adjuntos no Haskell são (,a)
e
Reader a = (a ->)
. Podemos definir a instância como:
instance Adjunction (,a) (Reader a) where
-- unit :: c -> Reader a (c,a)
unit x = \a -> (x, a)
-- counit :: (Reader a c, a) -> c
counit (f, x) = f x
Podemos definir leftAdjunct
e rightAdjunct
automaticamente como:
-- leftAdjunct :: ((x,a) -> y) -> x -> a -> y
leftAdjunct g = \x -> (fmap g . unit) x
= \x -> (fmap g) (unit x)
= \x -> (fmap g) (\a -> (x, a))
= \x -> g . (\a -> (x, a))
= \x -> \a -> g (x,a)
-- rightAdjunct :: (x -> (a -> y)) -> (x,a) -> y
rightAdjunct g (x,a) = counit . (fmap g) (x,a)
= counit (g x, a)
= g x a
Podemos perceber que leftAdjunct = curry
e rightAdjunct = uncurry
.
Lembrando que (,a) = Writer a
e, partindo da definição de Functors
Adjuntos, podemos criar dois novos Functors que é a composição de
Reader
com Writer
:
-- State a b = Reader a (Writer a b)
type State a b = a -> (b,a)
-- Store a b = Writer (Reader a b) a
type Store a b = (a -> b, a)
que permitem a criação de estados e armazenamento em uma linguagem puramente funcional. Esses Functors serão explorados em mais detalhes quando chegarmos em Monads.
Podemos pensar nos Functors adjuntos
Um exemplo desse tipo de Functors adjuntos em pseudo-Haskell seria:
instance Adjunction [] Mon where
unit :: a -> Mon [a]
unit x = [x]
counit :: [Mon a] -> a
counit = getMon . mconcat
leftAdjunct :: ([a] -> b) -> (a -> Mon b)
leftAdjunct f = fmap f . unit
rightAdjunct :: (a -> Mon b) -> ([a] -> b)
rightAdjunct f = counit . fmap f
Sendo Mon
um Functor representando um Monoid. Veja que []
é a
construção universal de um Monoid livre, enquanto Mon
utiliza []
mais algumas definições para gerar novos Monoids (esquecendo a estrutura
de lista). Essa ideia é utilizada para a criação de fold fusion, ou
seja, otimização do pipeline de um MapReduce.
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ http://blog.higher-order.com/assets/AdjunctionsSbtBExtended.pdf