ADT

Esse post é baseado no livro Teoria das Categorias para Programadores, de Bartosz Milewski.

1 Tipos de Dados Algébricos

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.

2 Tipo Produto

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.

3 Tipo Soma

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.

3.1 Funções que podem falhar

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)

4 Algebra dos Tipos

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.

5 Tipos Recursivos

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.

6 Herança de Classe e Tipo Soma

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.

7 Tipos Buracos

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")

8 Referências

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ http://strictlypositive.org/diff.pdf