Esse post é baseado no livro Teoria das Categorias para Programadores, de Bartosz Milewski.
Até então definimos a categoria \(\mathbf{Hask}\) como a categoria
contendo todos os tipos simples e compostos da linguagem de programação
Haskell. Além dos tipos mais conhecidos como
Int, Char, Bool, Float, Double vimos dois tipos especiais: Void, ()
que representam o tipo sem valor e o tipo com um único valor. Finalmente
aprendemos sobre o Tipo Produto e o Tipo Soma (coproduto).
Veremos nesse post que podemos fazer operações algébricas com esses tipos para criar tipos mais complexos e definir equivalência entre dois tipos, levando a simplificação desses. Tudo isso seguindo a mesma trilha de composição.
Revisitando o Tipo Produto, no Haskell e no Python ele é representado essencialmente por uma tupla de valores:
prod :: (Int, Bool)
prod = (42, True)
prod = (42, True)
E em C++ podemos utilizar o tipo pair:
pair<int, bool> p = make_pair(42, true);
Podemos perceber que a definição do tipo produto é comutativa até o
isomorfismo, ou seja, dado o par (Int, Bool) precisamos encontrar duas
funções:
f :: (Int, Bool) -> (Bool, Int)
g :: (Bool, Int) -> (Int, Bool)
tal que
f . g = id
g . f = id
Tanto a função f como a g são definidas de forma genérica através da
função swap:
swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)
É fácil perceber que aplicar duas vezes essa função retorna o estado original. Podemos dizer que essas duas tuplas armazenam informação de uma forma diferente uma da outra.
Um tipo produto não necessariamente precisa conter dois tipos, podemos
definir produtos de mais tipos fazendo um “produto de produtos”, por
exemplo, (Int, (Bool, Int)).
Exercício. O tipo produto ((Int, Bool), Int) é isomórfico com o tipo
(Int, (Bool, Int))? Defina duas funções que converta uma em outra e
sejam inversas.
Exercício. Fazendo a = Int como a quantidade de valores contidos no
tipo Int e, analogamente, b = Bool como a quantidade de valores no
tipo Bool. Quantos valores possui o tipo (Int, Bool)?
Para cada um dos valores de Int, podemos pareá-lo com todos os valores
de Bool, logo teremos \(a \cdot b\) valores.
A relação entre ((Int, Bool), Int) e (Int, (Bool, Int)) remete a
propriedade associativa da multiplicação em que
\((a \cdot b) \cdot c = a \cdot (b \cdot c) = a \cdot b \cdot c\) e,
realmente, podemos representar essa tripla como (Int, Bool, Int).
Na multiplicação também temos o elemento neutro, na álgebra representado
pelo valor \(1\), ou seja, \(x \cdot 1 = 1 \cdot x = x\). Qual tipo no
Haskell representa o valor \(1\)? É o unit (). Vamos verificar se
(a, ()) = ((), a) = a:
f :: (a, ()) -> a
f (x, ()) = x
g :: a -> (a, ())
g x = (x, ())
f . g = id
g . f = id
Ou seja, o tipo (a, ()) (e analogamente ((), a)) são isomórficos a
a, pois carregam a mesma informação.
No Haskell, podemos representar pares utilizando nomes específicos para diferenciar um par de outro:
data Circunferencia = Circ Double Double Double
data TrianguloRetangulo = Tri Double Double Double
Nesse código Circunferencia é o nome do tipo criado e Circ é o nome
do construtor desse tipo:
Circ :: Double -> Double -> Double -> Circunferencia
Notem que tanto o nome do tipo como o construtor podem ter o mesmo nome pois vivem em espaços de nomes diferentes.
Embora os tipos Circunferencia e TrianguloRetangulo sejam
isomórficos, no Haskell um não pode ser utilizado no lugar do outro
(como poderiam em Python e C++):
area :: Circunferencia -> Double
area (Circ xc yc r) = pi*r*r
tri :: TrianguloRetangulo
tri = Tri 10.0 10.0 5.0
z = area tri
Esse código apresentará um erro de compilação, pois o Haskell exige que os tipos da assinatura de função e seus argumentos sejam os mesmos. Por isso uma frase comum entre programadores Haskell é que “if a Haskell program compiles, it probably works” pois o sistema de tipos da linguagem impede que você passe argumentos para funções que sejam isomórficos porém representam diferentes contextos.
Essa ideia é atualmente estudada com o nome de Type-driven Development, em que o objetivo é dificultar a compilação de um programa de tal forma que, quando ele compila corretamente, minimiza as chances de bugs. No exemplo acima, embora os dois tipos podem conter a mesma informação, cada um só pode ser utilizado em seu contexto. Em outro exemplo, imagine que você está trabalhando com dois sistemas de coordenadas distintos, mas ambas representadas por dois valores. Cada uma delas tem um cálculo diferente de distância entre pontos. Fazendo essa distinção através da tipagem impede de utilizar descuidadamente um tipo de coordenada, no cálculo da distância de outro.
Uma outra forma de representar um novo tipo produto em Haskell, mais
similar aos struct do C/C++ é o tipo registro:
data Circunferencia = Circ { x_center :: Double
, y_center :: Double
, radius :: Double }
area :: Circunferencia -> Double
area c = pi*r*r where r = radius c
Note que em C++ não podemos declarar uma variável do tipo void (apenas
ponteiro para void) e, portanto, não podemos verificar as propriedades
algébricas do tipo produto. Em Python podemos utilizar o valor de None
livremente e podemos replicar os códigos acima.
No Haskell a forma canônica de implementar um tipo soma é através do
Either:
data Either a b = Left a | Right b
que pode ser lido como o tipo Either ou contém um valor do tipo a
ou um valor do tipo b. Da mesma forma que no tipo produto, podemos
calcular a quantidade de valores nesse tipo aplicando a operação de
soma, ou seja, o tipo Either contém \(a + b\) valores ao todo. Assim
como no tipo produto, podemos criar outros tipos soma além do já
fornecido:
data Forma = Circunferencia | TrianguloRetangulo
Também verificamos que a soma é associativa \((a + b) + c = a + (b + c) = a + b + c\) então temos que os dois tipos são isomórficos a:
data UmDosTres a b c = Um a | Dois b | Tres c
E também temos um elemento neutro, o Void (sem representantes em C++
ou Python):
Either a Void
É fácil perceber que nesse caso só podemos construir um elemento do tipo
Left a, ou seja, o tipo é isomórfico a a.
O tipo soma mais simples é a soma de tipos unit definidos como:
data Janken = Pedra | Papel | Tesoura
O construtor Pedra define seu próprio valor assim como o unit (),
a quantidade de valores do tipo Janken é então \(1 + 1 + 1 = 3\). Esse
tipo é equivalente ao enum do C++ e do Python:
enum {Pedra, Papel, Tesoura};
from enum import Enum
class Janken(Enum):
Pedra = 1
Papel = 2
Tesoura = 3
for j in Janken:
print(j)
Um outro exemplo de tipo soma no Haskell é o tipo Bool definido como:
data Bool = True | False
E definido internamente no C++ e Python como o tipo bool.
Vimos anteriormente que algumas funções podem não ser totais em seu tipo
de entrada como, por exemplo, a função sqrt. A assinatura dessa
função, em sua forma canônica é:
sqrt :: Double -> Double
Equivalente em C++:
double sqrt(double);
Como podemos definir o tipo de saída para que ele indique a ausência de uma resposta? Algumas soluções comuns em C++ são:
double safe_sqrt (double x) {
// retorna um valor impossível para representar falha
if (x < 0) return -1;
return sqrt(x);
}
double * safe_sqrt (double x) {
double * answer;
if (x < 0) return NULL;
answer = new double;
*answer = sqrt(x);
return answer;
}
char safe_sqrt (double x, double * answer) {
if (x < 0) return 0;
*answer = sqrt(x);
return 1;
}
Pensando em uma solução mais segura, utilizando tipos algébricos,
podemos pensar em, dado um tipo a, acrescentar mais um valor que
sinalize a ausência de informação, ou seja, precisamos de um tipo
a + 1. Com isso podemos criar o tipo Maybe definido, por exemplo,
como:
data Maybe a = Either () a
e nossa função fica definida como:
safeSqrt :: Double -> Maybe a
safeSqrt x | x < 0 = Left ()
| otherwise = Right (sqrt x)
O tipo Maybe no Haskell é, na verdade, definido como
data Maybe a = Nothing | Just a, que é isomórfico a Either () a. No
C++14 temos a estrutura optional:
#include <experimental/optional>
using namespace std;
using namespace experimental;
optional<double> safe_root(double x) {
if (x >= 0) return optional<double>{sqrt(x)};
else return optional<double>{};
}
E, em Python, podemos utilizar None:
def safe_root(x):
if (x < 0) return None
return sqrt(x)
Vimos até agora que os tipos Soma e Produto apresentam elementos nulos e neutros, ou seja:
-- a * 0 = 0
data Absurdo a = Ab a Void = Void
-- a * 1 = a
data Unity a = U a () = a
-- a + 0 = a
data Soma0 a = a | Void = a
Esses tipos também possuem propriedades distributivas entre eles? Ou seja, podemos pensar que \(a \cdot (b + c) = a \cdot b + a \cdot c\)? Vejamos:
type Alpha a b c = (a, (Either b c))
type Beta a b c = Either (a, b) (a, c)
f :: Alpha -> Beta
f (x, Left y) = Left (x, y)
f (x, Right y) = Right (x, y)
g :: Beta -> Alpha
g Left (x, y) = (x, Left y)
g Right (x, y) = (x, Right y)
E a composição forma a identidade, portanto os dois tipos são
isomórficos. Nesse ponto, é fácil perceber que os tipos Soma e Produto
podem ser compostos para formar outros tipos mais complexos (o tipo
Forma é um exemplo).
Em Haskell, a convenção é de fazermos soma de produtos, ou seja, um tipo \((a + b) \cdot (c + d)\) é transformado em um tipo \((a \cdot c + a \cdot d + b \cdot c + b \cdot d)\):
data Tipo a b c d = T (Either a b) (Either c d)
data SomaProd a b c d = Um a c | Dois a d | Tres b c | Quatro b d
Embora o segundo pareça ser mais complicado, quando fazemos pattern matching em uma função, a separação das possibilidades de um tipo soma simplifica a definição de uma função:
f :: Tipo Int Int Int Int -> Int
f (T Left x) (T Left y) = x
f (T Left x) (T Right y) = x
f (T Right x) (T Left y) = y
f (T Right x) (T Right y) = x
f :: SomaProd Int Int Int Int -> Int
f (Um x y) = x
f (Dois x y) = x
f (Tres x y) = y
f (Quatro x y) = x
Tanto o tipo Soma como o tipo Produto formam um Monoid:
instance Monoid Soma where
mempty = Void
mappend = Either
instance Monoid Prod where
mempty = ()
mappend = (,)
A combinação desses dois Monoids formam um semi-anel pois suporta a operação de soma e produto, mas não contém a definição de valores negativos. Com isso temos a seguinte tabela de equivalência entre a algebra e os tipos soma e produto:
| Algebra | Tipos |
|---|---|
| \(0\) | Void |
| \(1\) | () |
| \(a + b\) | Either a b |
| \(a * b\) | (a, b) |
| \(2 = 1 + 1\) | Bool = True \vert False |
| \(1 + a\) | Maybe a = Nothing \vert Just a |
Da mesma forma que os tipos em Haskell são isomórficos ao semi-anel da álgebra, eles também são isomórficos com a lógica clássica:
| Lógica | Tipos |
|---|---|
| Falso | Void |
| Verdadeiro | () |
| \(a \lor b\) | Either a b |
| \(a \land b\) | (a, b) |
Esse isomorfismo é conhecido como Isomorfismo de Curry-Howard e pode ser estendido para categorias.
Uma outra forma interessante de construção de tipos é através da recursão. Por exemplo, considere o tipo que representa uma lista em Haskell:
data List a = Vazio | (:) a (List a)
Essencialmente isso nos permite definir uma lista como:
xs = List Int
xs = 1 : 2 : 3 : Vazio
que representa a lista [1,2,3]. Percebemos que essa é a definição de
uma lista ligada, com o operador (:) apontando para o próximo
elemento. Em C++ podemos fazer isso utilizando struct:
template<class A>
class List;
template<class A>
struct Node {
Node(A a, List<A> l) {value=a; next=l;};
A value;
List<A> next;
};
ou utilizando o truque do nullptr em forma de uma classe:
template<class A>
class List {
Node<A> * _head;
public:
List() : _head(nullptr) {} // Nil
List(A a, List<A> l) // Cons
: _head(new Node<A>(a, l))
{}
Node<A> * notEmpty() {return _head;}
A head() {return _head->value;}
List<A> * tail() {return _head ? &(_head->next) : nullptr;};
};
Nesse caso, a classe List pode ser criada com um entre dois
construtores, um que não recebe argumento e retorna um ponteiro nulo
para _head, e outro que recebe um elemento do tipo A e uma lista,
armazenando um ponteiro para Node contendo tal elemento e um ponteiro
para o restante da lista. Nessa classe, o tipo Node é implementado de
forma similar a struct Node.
Em Python, podemos fazer algo similar com C++:
class List:
def __init__(self, x=None, l=None):
if x is None:
self.head = None
self.head = (x, l)
lista = List(1, List(2, List(3, List(None))))
while lista is not None:
(x, lista) = lista.head
print(x)
Quantos valores possíveis temos para um tipo List a? Podemos resolver
isso algebricamente também definindo x = List a:
\(x = 1 + a \cdot x\)
\(x = 1 + a \cdot (1 + a \cdot x)\)
\(x = 1 + a + a^2 \cdot x\)
\(x = 1 + a + a^2 + a^3 \cdot x\)
\(x = 1 + a + a^2 + a^3 + a^4 + \ldots\)
Esse resultado pode ser interpretado como:
Uma lista do tipo a pode conter um único valor (lista vazia) ou um valor do tipo a ou dois valores do tipo a, etc.
Digamos que precisamos criar um tipo Shape que permite o cálculo da
área e circunferência de diversas formas. Em C++ e Python, utilizamos
herança para definir essa abstração:
class Shape {
public:
virtual double area() = 0;
virtual double circ() = 0;
};
class Circle : public Shape {
public:
double area() { return PI*r*r; }
double circ() { return 2.0*PI*r; }
void set_radius(double radius) {r=radius;};
protected:
double r;
};
class Rect : public Shape {
public:
double area() { return w*h; }
double circ() { return 2.0*(w+h); }
void set_sides(double wi, double hi) {w=wi; h=hi;};
protected:
double w;
double h;
};
class Square : public Shape {
public:
double area() { return s*s; }
double circ() { return 4.0*s; }
void set_side(double si) {s=si;};
protected:
double s;
};
class Shape(ABC):
@abstractmethod
def area(self):
pass
@abstractmethod
def circ(self):
pass
class Circle(Shape):
def __init__(self, r):
self.r = r
def area(self):
return pi*self.r*self.r
def circ(self):
return 2.0*pi*self.r
class Rect(Shape):
def __init__(self, w, h):
self.w = w
self.h = h
def area(self):
return self.w * self.h
def circ(self):
return 2.0*(self.w + self.h)
class Square(Shape):
def __init__(self, s):
self.s = s
def area(self):
return self.s*self.s
def circ(self):
return 4.0*self.s
Com a definição de um tipo soma podemos fazer essa mesma abstração utilizando simplesmente a funcionalidade de Pattern Matching:
data Shape = Circle Float
| Rect Float Float
| Square Float
area :: Shape -> Float
area (Circle r) = pi * r * r
area (Rect d h) = d * h
area (Square s) = s * s
circ :: Shape -> Float
circ (Circle r) = 2.0 * pi * r
circ (Rect d h) = 2.0 * (d + h)
circ (Square s) = 4.0 * s
Com isso, a construção de uma nova forma exige a inclusão de poucas
linhas de código. Embora desabilitado por padrão, o usuário pode passar
a opção -fwarn-incomplete-patterns para o compilador avisar caso falte
a definição de alguma das formas para uma das funções.
O que mais podemos fazer com os tipos algébricos? Uma outra operação possível é o cálculo da derivada de nossos tipos. A derivada de uma função representa a variação instantânea de uma variável, na álgebra dos tipos ela representa o foco em um determinado componente do nosso tipo algébrico.
Vamos estabelecer algumas derivadas básicas em função de um tipo a:
()' = Void -- não tenho em que focar
a' = () -- a função () -> a foca em um valor de a
(a+b)' = () + Void = () -- foco em um elemento da esquerda
(a*b)' = 1*b = b -- fixa um elemento de a
(a*a)' = 2a = a + a -- fixa no primeiro ou segundo elemento da tupla
Uma aplicação para esses buracos em nossos tipos é em como fazer um percurso de forma eficiente em estruturas não-lineares. Começando com uma simples lista, sabemos que a sua representação algébrica é:
\(x = 1 + a \cdot x\)
Isolando a variável \(x\) temos:
\(x = 1/(1-a)\)
Derivando esse tipo, temos:
\(x’ = 1/(1-a)^2\)
que simplesmente representa o tipo produto de duas listas. Com isso
podemos criar a estrutura denominada Zipper pois permite percorrer a
lista como se fosse um zipper:
data Zipper a = Zip [a] [a]
criaZip :: [a] -> Zipper a
criaZip xs = Zip [] xs
esq :: Zipper a -> Zipper a
esq (Zip [] ds) = Zip [] ds
esq (Zip (e:es) ds) = Zip es (e:ds)
dir :: Zipper a -> Zipper a
dir (Zip es []) = Zip es []
dir (Zip es (d:ds)) = Zip (d:es) ds
Com isso definimos uma lista duplamente ligada:
xs :: [Int]
xs = [1,2,3,4,5]
zs :: Zipper Int
zs = criaZip xs
-- zs = Zip [] [1,2,3,4,5]
zs' :: Zipper Int
zs' = (dir . dir) zs
-- zs' = Zip [2,1] [3,4,5]
zs'' :: Zipper Int
zs'' = esq zs'
-- zs'' = Zip [1] [2,3,4,5]
Outro Zipper interessante é o de uma árvore com elemento apenas nos
nós internos:
data Tree a = Empty | Node (Tree a) a (Tree a)
A estrutura algébrica Tree a pode ser definida como
Tree a = 1 + a * (Tree a) * (Tree a), substituindo Tree a por \(x\),
temos:
\(x = 1 + a*x^2\)
Derivando em função de \(a\) temos:
\(x’ = x^2 + 2*a*x*x’\)
Que pode ser resolvido como:
\(x’ = (x^2)/(1 - 2ax) = x^2 \cdot 1/(1-2ax) = x^2 \cdot 1/(1 - (ax+ax))\)
Transformando em um tipo algébrico, isso representa o produto entre uma
tupla de árvores e uma lista do tipo Either (a, Tree a) (a, Tree a),
ou (Tree a, Tree a, [Either (a, Tree a)]). Vamos nomear cada parte
para facilitar o papel de cada termo dessa estrutura:
data Zipper a = Zip { left :: Tree a
, right :: Tree a
, focus :: [Either (a, Tree a) (a, Tree a)]
}
Então o foco em um elemento \(x\) de uma árvore binária com valores
apenas nos nós internos é composta pelos filhos da esquerda e direita do
nó foco, o nó em questão e uma lista de subárvores acima desse nó junto
com a informação Left, Right da direção que percorremos até chegar
nele. Com isso podemos definir:
criaZip :: Tree a -> Zipper a
criaZip Empty = Zip Empty Empty []
-- Foco inicial não tem ninguém acima dele (Empty)
criaZip (Node l x r) = Zip l r [Left (x, Empty)]
esq :: Zipper a -> Zipper a
esq tz = case left tz of
Empty -> tz -- se não temos nós a esquerda
-- O novo foco é o nó raiz da árvore esquerda
-- acima dele é a árvore direita
Node l x r -> Zip l r (Left (x, (right tz)) : focus tz)
dir :: Zipper a -> Zipper a
dir tz = case right tz of
Empty -> tz
Node l x r -> Zip l r (Right (x, (left tz)) : focus tz)
upwards :: Zipper a -> Zipper a
upwards (Zip l r []) = Zip l r []
upwards (Zip l r [x]) = Zip l r [x]
upwards (Zip l r (f:fs)) = t
where t = case f of
Left (x, t') -> Zip (Node l x r) t' fs
Right (x, t') -> Zip t' (Node l x r) fs
Com esse tipo de árvore podemos fazer um algoritmo de backtracking e forma eficiente:
\node (1) {$1$};
\node (2) [below left of=1] {$2$};
\node (4) [below left of=2] {$4$};
\node (5) [below right of=2] {$5$};
\node (3) [below right of=1] {$3$};
\draw[-] (1) edge (2);
\draw[-] (1) edge (3);
\draw[-] (2) edge (4);
\draw[-] (2) edge (5);
t :: Tree Int
t = Node (Node (Node Empty 4 Empty) 2 (Node Empty 5 Empty)) 1 (Node Empty 3 Empty)
tz :: Zipper Int
tz = criaZip t
-- Zip {left = Node (Node Empty 4 Empty) 2 (Node Empty 5 Empty)
-- , right = Node Empty 3 Empty
-- , focus = [Left (1,Empty)]}
esq tz
-- Zip {left = Node Empty 4 Empty
-- , right = Node Empty 5 Empty
-- , focus = [Left (2,Node Empty 3 Empty),Left (1,Empty)]}
(esq . esq) tz
-- Zip {left = Empty
-- , right = Empty
-- , focus = [Left (4,Node Empty 5 Empty),Left (2,Node Empty 3 Empty),Left (1,Empty)]}
(dir . esq . esq) tz
-- Zip {left = Empty
-- , right = Empty
-- , focus = [Left (4,Node Empty 5 Empty),Left (2,Node Empty 3 Empty),Left (1,Empty)]}
(upwards . esq) tz = tz
Em Python, esse mesmo código fica:
class Tree:
def __init__(self, x=None, left=None, right=None):
self.x = x
self.left = left
self.right = right
def __str__(self):
return f"({self.left} {self.x} {self.right})"
class Zipper:
def __init__(self, t):
self.left = t.left
self.right = t.right
self.focus = [(False, t.x, None)]
def __str__(self):
return f"#{self.left} # {self.right} # {self.focus}#"
def esq(self):
left, right = self.left, self.right
if left is not None:
self.left = left.left
self.right = left.right
self.focus.append((False, left.x, right))
return self
def dir(self):
left, right = self.left, self.right
if right is not None:
self.left = right.left
self.right = right.right
self.focus.append((True, right.x, left))
return self
def upward(self):
if len(self.focus) > 1:
(dir, x, t) = self.focus.pop(-1)
if dir:
self.right = Tree(x, self.left, self.right)
self.left = t
else:
self.left = Tree(x, self.left, self.right)
self.right = t
return self
n3 = Tree(3)
n4 = Tree(4)
n5 = Tree(5)
n2 = Tree(2, n4, n5)
n1 = Tree(1, n2, n3)
z = Zipper(n1)
print(z, "\n")
z.esq()
print(z, "\n")
z.esq()
print(z, "\n")
z.dir()
print(z, "\n")
z.upward().upward()
print(z, "\n")
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ http://strictlypositive.org/diff.pdf