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:

  1. Objeto terminal
  2. qualquer \(a, b \in C\) implica em \(a \cdot b \in C\) (a categoria possui tipo produto)
  3. 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:

  1. Objeto inicial
  2. 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/