Tipo Função
Esse post é baseado no livro Teoria das Categorias para Programadores, de Bartosz Milewski.
1 Tipo Função
Vimos anteriormente em Tipos de Dados Algébricos os tipos fundamentais e a construção de tipos mais complexos através do Tipo Soma, do Tipo Produto, e Tipos Recursivos. Esses tipos são algébricos pois, ao denotá-los como variáveis representando a cardinalidade do conjunto de seus valores, tais estruturas podem ser formadas através de operações algébricas de soma e multiplicação.
Em Teoria das Categorias, para uma categoria \(C\) definimos \(C(a, b)\) como o conjunto de morfismos iniciando em \(a\) e terminando em \(b\). Na categoria \(\mathbf{Hask}\) temos que um morfismo é uma função que recebe um argumento do tipo \(a\) e retorna um tipo \(b\). Se \(a \rightarrow b\) representa o conjunto de funções com essa assinatura, podemos definir um Tipo Função.
Para definir o tipo função, vamos utilizar a construção universal. O padrão que buscamos dentro de nossa categoria é formado por três objetos, um representando o nosso tipo função que iremos chamar de \(z\), e que contém diversas funções \(f\), um que representa o argumento da função, o tipo \(a\), e outro que representa o resultado da aplicação da função, ou tipo \(b\):
A conexão entre esses três objetos se dá pelo padrão conhecido pelos
programadores como aplicação de função ou avaliação de função. Esse
padrão pode ser escrito como: dado um tipo função \(z\) e um tipo de
entrada \(a\), o morfismo mapeia essa tupla em um tipo \(b\). Ou seja,
temos um tipo produto formado por \((z, a)\) e um morfismo
g :: (z, a) -> b.
Finalmente precisamos definir um rank para seleconar o melhor \(z\)
entre todos os candidatos. Para isso definimos que um \(z\) é melhor que
um \(z’\) caso exista um morfismo h :: z' -> z que fatora \(g’\) em
\(g\), ou seja, podemos definir \(g’\) em função de \(h\).
Para isso a fatoração deve funcionar no par \((z’, a)\) transformando em
um par \((z, a)\). Já sabemos que a transformação de um tipo produto
(a, b) para um tipo (c, d) é feito através de um Bifunctor, nesse
nosso caso temos bimap = (h, id) :: (z', a) -> (z, a). Com isso
conseguimos definir g' = g . (h, id).
Finalmente vamos encontrar o melhor entre todos os candidatos de \(z\).
Vamos chamar o melhor \(z\) como \(a \implies b\) e o melhor \(g\) como
eval (de function evaluation). Com isso temos
Um objeto função de a para b é denominado \(a \implies b\) junto com o morfismo eval :: ((a => b), a) -> b tal que para qualquer outro objeto \(z\) com um morfismo g :: (z, a) -> b existe um único morfismo h :: z -> (a => b) que g = eval . (h, id).
2 Currying
Imagine que escolhemos um certo objeto \(z\) acompanhado de seu morfismo \(g\). O morfismo pode ser interepretado como uma função de dois argumentos \((z, a)\) que retorna um \(b\):
g :: (z, a) -> b
Sabemos que a melhor escolha de objeto pode ser encontrada através da
aplicação de \(h\), que transforma nosso \(z\) em um a -> b:
h :: z -> (a -> b)
Dizemos que \(h\) é uma função que recebe um objeto do tipo \(z\) e
retorna uma função de \(a\) para \(b\), é uma função de alta ordem. Isso
nos diz que toda função de dois argumentos é, na verdade, uma função de
um argumento que retorna outra função. Isso é conhecido como currying,
dizemos que h é a forma curried de g. Podemos definir a forma
uncurried utilizando nosso morfismo eval, que reconstrói nosso g:
g = eval . (h, id) :: (z, a) -> b
Ou seja, essas definições são isomórficas. Em Haskell todas as versões de múltiplos argumentos são naturalmente interpretadas como sua versão curry:
a -> (b -> c) = a -> b -> c
Isso fica claro na definição de uma função de duas variáveis em Haskell:
mult :: Int -> Int -> Int
mult x y = x*y
mult' :: Int -> (Int -> Int)
mult' x = \y -> x*y
Que se torna evidente quando fazemos uma aplicação parcial da primeira função:
dobra = mult 2
dobra :: Int -> Int
A biblioteca padrão do Haskell já tem a conversão das duas formas de definição de funções:
curry :: ((a, b)->c) -> (a->b->c)
curry f a b = f (a, b)
uncurry :: (a->b->c) -> ((a, b)->c)
uncurry f (a, b) = f a b
Em C++ você pode fazer uma aplicação parcial de função utilizando o
template std::bind:
int mult(int x, int y) {
return x*y;
}
using namespace std::placeholders;
auto dobra = std::bind(mult, 2, _1);
std::cout << dobra(4);
Em Python temos a função partial:
from functools import partial
def mult(x,y):
return x * y
dobra = partial(mult, 2)
3 Tipo de Dados Algébrico Exponencial
A interpretação algébrica de um tipo função é a de um exponencial. Isso
se torna evidente com uma função do tipo Bool para um certo tipo a e
outra função de um tipo a para Bool:
f :: Bool -> a
g :: a -> Bool
De quantas maneiras podemos definir a função f? A entrada é definida
pelos dois possíveis valores True e False, ou seja, podemos dizer
que uma função de Bool para a é definida por um par de valores de
a. Já vimos isso anteriormente quando percebemos que Bool -> a é
isomórfica a (a, a). Com isso temos a^2 definições diferentes para
essa função.
A função g deve definir um valor True ou False para cada um dos
valores de a, ou seja, é uma tupla (Bool, Bool, Bool, ..., Bool) com
a elementos. Analogamente, isso é equivalente a 2^a possíveis
definições.
O tipo função a -> b é representada por uma exponencial b^a,
indicando as possíveis combinações de entrada e saída para essa
assinatura de função.
Vamos verificar se esse tipo também obedece as propriedades algébricas de uma exponenciação.
3.1 Potência de Zero
Uma função \(a^0 = 1\) tem a assinatura:
f :: Void -> a
que já vimos possuir apenas uma definição que é a função absurd.
3.2 Potência envolvendo Um
Analogamente, uma função \(a^1 = a\) tem a assinatura:
f :: () -> a
que é a função unit que seleciona um valor de a, portanto possui a
definições diferentes.
Já a função \(1^a = 1\) tem como assinatura e única definição:
const :: a -> ()
const x = ()
3.3 Somas de Exponenciais
Uma função \(a^{b+c}\) é uma função de um tipo soma para um tipo a:
f :: Either b c -> a
f (Left x) = ...
f (Right y) = ...
Ou seja, é uma função que deve ser definida para os casos b -> a e
c -> a. Em outras palavras devemos definir um par de funções, o que é
compatível com a propriedade da exponenciação
\(a^{b+c} = a^b \cdot a^c\).
3.4 Exponenciais de Exponenciais
Uma função \((a^b)^c\) é interpretada como uma função que recebe um tipo
c e retorna uma função de b -> a, ou seja, uma função de alta ordem:
f :: c -> (b -> a)
Mas sabemos que essa forma é equivalente a uma função que recebe um par
(c, b) e retorna um a. Ou seja, \((a^b)^c = a^{(bc)}\)
3.5 Exponenciais sobre produtos
Também podemos ter uma função \((a \cdot b)^c\) que é representada por:
f :: c -> (a, b)
Isso é equivalente a um par de funções c -> a e c -> b (nossas
funções p, q do tipo produto) que nos dá
\((a \cdot b)^c = a^c \cdot b^c\)
4 Cartesian Closed Category
Uma Categoria que possui:
- Objeto terminal
- qualquer \(a, b \in C\) implica em \(a \cdot b \in C\) (a categoria possui tipo produto)
- qualquer \(a, b \in C\) implica em \(a^b \in C\)
Dizemos que é uma Categoria Cartesiana Fechada (CCC). Se além disso ela tiver as propriedades complementares:
- Objeto inicial
- qualquer \(a, b \in C\) implica em \(a+b \in C\)
Então ela é uma Categoria Bicartesiana Fechada (Bicartesian Closed Category - BCCC).
5 Isomorfismo de Curry Howard
Complementando nossa tabela do isomorfismo de Curry Howard temos:
| Algebra | Tipos | Lógica |
|---|---|---|
| \(0\) | Void |
Falso |
| \(1\) | () |
Verdadeiro |
| \(a + b\) | Either a b | \(a \lor b\) |
| \(a * b\) | (a, b) | \(a \land b\) |
| \(b^a\) | \(a \rightarrow b\) | \(a \implies b\) |
A definição de uma função é isomórfica a definição de uma implicação.
Por exemplo, nossa função eval com assinatura:
eval :: ((a->b), a) -> b
Pode ser traduzida como: “Se b segue de a e a é verdadeiro, então
b é verdadeiro.”. Provamos essa proposição implementando, ou seja,
mostrando que esse tipo é habitável por algum valor:
eval :: ((a->b), a) -> b
eval (f, x) = f x
Vamos tentar provar a proposição \((a \lor b) \implies a\), ou seja, se \(a\) ou \(b\) forem verdadeiros, então \(a\) é verdadeiro:
f :: Either a b -> a
f (Left x) = x
f (Right y) = ???
Na segunda definição eu tenho que prover uma expressão que funcione para qualquer que seja o tipo \(a\). Impossível!
Podemos então usar funções definidas em Haskell como provas de proposições lógicas.
6 Referências
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/