Esse post é baseado no livro Teoria das Categorias para Programadores, de Bartosz Milewski.
Quando estudamos uma categoria, não olhamos para dentro de seus objetos, diferenciamos um dos outros através do padrão de morfismos que partem ou chegam nele. Os morfismos são os atores principais de uma categoria conforme veremos ao longo das próximas postagens.
Para selecionar objetos de interesse utilizamos a construção universal, primeiro definimos um padrão de interesse e, em seguida, uma forma de rankear os objetos que obedecem tal padrão. Com isso podemos selecionar um objeto específico que apresenta propriedades de interesse.
Um conceito importante quando comparamos dois objetos é a ideia de igualdade. Na programação o que significa dois objetos serem iguais?
x, y
são iguais se apontam para
o mesmo endereço).struct
ou class
,
p. ex.) são iguais?Dada a dificuldade em determinar se dois objetos são iguais (por não termos uma definição concreta de igualdade), podemos pensar em uma relação mais fraca, a de isomorfismo.
Dois objetos são isomórficos se eles apresentam o mesmo formato, ou seja, existe uma equivalência de cada valor de um objeto para o valor do outro objeto. Matematicamente, existe um mapa de \(a \rightarrow b\) que mapeia cada elemento de \(a\) para um elemento de \(b\) e, da mesma forma, um mapa \(b \rightarrow a\), sendo um o inverso do outro. Ambas as funções devem ser bijetivas.
Relembrando, uma função injetiva é quando dois ou mais elementos do domínio não podem ser mapeadas para um mesmo elemento do co-domínio. Função sobrejetiva é aquela em que todo elemento do co-domínio é o mapeamento de pelo menos um elemento do domínio. Função bijetiva é toda função injetiva e sobrejetiva. Ou seja, a função bijetiva existe entre dois conjuntos de mesmo tamanho e que cada elemento do conjunto co-domínio está relacionado com um elemento do domínio.
Podemos pensar em isomorfismo entre um objeto \(a\) e outro objeto \(b\)
em termos de seus morfismos se existem dois morfismos f : a -> b
e
g : b -> a
, tal que:
f . g = id
g . f = id
Graficamente temos:
Pensando na categoria da pré-ordem, podemos definir a noção de que um objeto \(a\) é “mais anterior” a outro objeto \(b\) se existe uma seta \(a \rightarrow b\). Dessa forma podemos pensar no objeto que é o mais anterior a todos os outros, o objeto inicial.
O objeto inicial é aquele que apresenta um e apenas um morfismo para todos os outros objetos da categoria.
Esse objeto, se existir, é único até o isomorfismo, ou seja, na existência de dois objetos com essa propriedade, um pode ser mapeado no outro sem perda de informação.
Na categoria de ordem parcial, o objeto inicial é o menor elemento. Já na categoria dos conjuntos (\(\mathbf{Set}\)) esse objeto é o conjunto vazio com os morfismos sendo o funções vazias.
Na categoria dos tipos do Haskell (\(\mathbf{Hask}\)), esse objeto é o
Void
(que não tem nenhum equivalente em C++ ou Python) e o morfismo,
já vimos anteriormente, é:
absurd :: Void -> a
De forma similar, podemos definir que o objeto \(a\) é “mais terminal” que \(b\) se existe um morfismo entre \(b \rightarrow a\) (nota: o complemento de um padrão em teoria das categorias é a inversão das setas nos morfismos). Com isso definimos o objeto terminal.
O objeto terminal é aquele com um e apenas um morfismo chegando até ele a partir de qualquer outro objeto.
Esse objeto também deve ser único até o isomorfismo.
Na categoria de ordem parcial, o objeto terminal é o maior elemento da categoria. Na categoria dos conjuntos temos que todos os singletons representam um objeto terminal, sendo os morfismos um mapa entre todos os elementos de um conjunto apontando para um único elemento do singleton.
Finalmente, em \(\mathbf{Hask}\), esse objeto é o unit ()
que,
similar à categoria dos conjuntos, temos a definição:
unit :: a -> ()
unit _ = ()
Poderíamos pensar também que o objeto Bool
também serve como objeto
inicial uma vez que temos:
sim :: a -> Bool
sim _ = True
Porém temos uma segunda função de todos os objetos para Bool
:
nao :: a -> Bool
nao _ = False
Como nossa condição é a de que existe apenas uma única função entre o
objeto terminal e todos os outros objetos, o Bool
não é um objeto
inicial.
Vamos verificar que realmente ()
e Bool
não são isomórficos.
Assumindo que ambos ()
e Bool
são terminais, significa que temos um
único morfismo f : () -> Bool
e um morfismo g : Bool -> ()
. Para
eles serem isomórficos, um necessariamente tem que ser o inverso do
outro (não temos outra opção):
f : () -> Bool
f () = True
g : Bool -> ()
g _ = ()
(g . f) () = ()
(f . g) True = True
(f . g) False = True
Como podemos perceber, mesmo com a outra definição de a -> Bool
não
temos isomorfismo
Notem que o unit não pode ser um objeto inicial pois para isso precisariamos definir uma função do tipo:
impossivel :: () -> a
impossivel () = ??
A assinatura do Haskell deve ser interpretada como uma afirmação forte, ou seja:
f :: a -> ()
deve ser lida como: “Existe uma definição f
que, para qualquer tipo
a
, ele mapeia para o unit
. E ao apresentar tal defininição, estamos
na verdade provando essa afirmação:
f :: a -> ()
f x = ()
Voltando a nossa função impossivel
, não temos como definir essa função
de tal forma que ele retorne um valor que pertença a todo e qualquer
tipo de \(\mathbf{Hask}\).
É interessante observar que a definição de objeto inicial e objeto terminal são duais, a única diferença entre as duas é a direção das setas dos morfismos envolvidos. Para toda categoria \(C\) podemos definir a categoria oposta \(C^{OP}\) que é exatamente igual a \(C\), porém com a direção de todos os morfismos invertida.
Se temos morfismos \(f : a -> b\) e \(g : b -> c\) compostas como \(g . f = h : a -> c\) na categoria \(C\), teremos os morfismos \(f^{OP} : b -> a\) e \(g^{OP} : c -> b\) que formam \(f^{OP} . g^{OP} = h^{OP} : c -> a\).
Os conceitos duais em teoria das categorias costumam ser prefixados com “co”, conforme veremos em seguida com produtos e coprodutos.
Outra construção universal importante é o conceito de produto. Sabemos que o produto cartesiano de dois conjuntos é um conjunto de pares. Mas qual o padrão de morfismos que definem esses pares?
Dado um produto, podemos definir duas funções de projeção que projetam o par para um de seus elementos. Em Haskell podemos definir da seguinte forma:
fst :: (a, b) -> a
fst (x, _) = x
snd :: (a, b) -> b
snd (_, y) = y
Em C++, podemos definir tais funções utilizando templates:
template<class A, class B>
A fst(pair<A, B> const & p) {
return p.first;
}
template<class A, class B>
A snd(pair<A, B> const & p) {
return p.second;
}
E em Python de forma genérica:
def fst(x):
return x[0]
def snd(x):
return x[1]
Vamos assumir \(c\) como sendo nosso tipo produto proveniente do produto de um tipo \(a\) com um tipo \(b\). Com isso precisamos definir duas funções:
p :: c -> a
q :: c -> b
Temos diversos candidatos para esse padrão. Pensando no par Int
e
Bool
, podemos definir c :: Int
fazendo:
p :: Int -> Int
p x = x
q :: Int -> Bool
q _ = True
Outro candidato é fazer com que c :: (Int, Int, Bool)
:
p :: (Int, Int, Bool) -> Int
p (x, _, _) = x
q :: (Int, Int, Bool) -> Bool
q (_, _, b) = b
Precisamos definir um rank para indicar o melhor candidato possível. Podemos dizer que se possuímos dois candidatos \(c, c’\) com seus morfismos \(p, q, p’, q’\), dizemos que \(c\) é melhor que \(c’\) se existir apenas um único morfismo \(m\) tal que:
m :: c' -> c
p' = p . m
q' = q . m
Pensando na opção \(c = (Int, Bool)\) e nas alternativas anteriores, podemos fazer:
m1 x = (x, True)
m2 (x, _, b) = (x, b)
Vamos tentar fazer o oposto agora, encontrar um m2'
que converta c
na segunda opção de c'
:
m2' (x, b) = (x, 1, b)
mas também podemos fazer:
m2' (x, b) = (x, 2, b)
e tantos outros, então m2'
não possui uma única definição possível.
Dessa forma percebemos que a tupla/par (a, b)
é nossa melhor opção
para um tipo produto.
O tipo produto de dois objetos a
e b
é o objeto c
equipado com duas projeções de tal forma que qualquer outro objeto c'
com duas projeções para a
e b
, existe um único morfismo m
de c'
para c
que fatora as projeções.
Vamos pensar agora no padrão dual ao produto, chamado coproduto:
i :: a -> c
j :: b -> c
A fatoração para rankeamento do melhor tipo para definir o coproduto é:
m :: c -> c'
i' = m . i
j' = m . j
O tipo coproduto ou tipo soma de dois objetos a
e b
é o objeto c
equipado com duas funções injetivas tal que para qualquer objeto c'
também equipado com duas injeções, existe um único morfismo m
de c
para c'
que fatora as funções injetivas.
Podemos pensar no coproduto como uma união disjunta de dois conjuntos. Em Haskell podemos definir um tipo soma como:
data C = A Int | B Bool
Lemos essa definição como “O tipo C
é composto de ou um componente
A
do tipo Int
ou um componente B
do tipo Bool
. Uma forma mais
genérica é obtida pelo tipo paramétrico Either
:
data Either a b = Left a | Right b
Em C++ implementamos o tipo soma como um tagged union:
template<class A, class B>
struct Either {
enum { isLeft, isRight } tag;
union { A left; B right; };
};
Finalmente, em Python podemos fazer:
class Either:
def __init__(self):
left = right = None
def add_left(self, x):
self.left = x
self.right = None
def add_right(self, x):
self.left = None
self.right = x
def get_val(self):
if self.left is not None:
return (self.left, "L")
if self.right is not None:
return (self.right, "R")
return (None, "LR")
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/