Introdução aos Tipos Dependentes

Overview

No mundo da programação funcional, uma ideia introduzida há algum tempo vem ganahando força. É a tipagem dependente: tipos que dependem de valores. O tipo de par ordenado (n : Natural) ⨯ (Vetor a n) é um exemplo de tipo dependente. O primeiro elemento do par é um número natural n. O segundo elemento é um vetor que armazena valores do tipo a e cujo tamanho é aquele mesmo número natural n. Estabelecemos uma relação de dependência entre um tipo e um valor. O primeiro elemento do par é sempre o tamanho do vetor.

O mais surpreendente é que toda a tipagem e as dependências são apagadas em tempo de execução. Não é necessário o operador instanceof do Java ou qualquer função getType x. É tudo feito com análise estática sobre o código. A linguagem Idris até disponibiliza reflexão em tempo de execução, mas essa feature tem a intenção de ser usada com meta programação, e não tem muita relação com a tipagem dependente.

A maior parte das linguagens com tipos dependentes são funcionais porque linguagens funcionais costumam ser mais fáceis de serem formalizadas. Existem linguagens que têm proposta de adicionar tipos dependentes à programação imperativa, mas muitas delas têm partes funcionais. Uma delas é ATS (Applied Type System), que busca ser uma alternativa safe a C por meio de tipos dependentes e tipos lineares.

Botando as Mãos na massa

Farei uma pequena demonstração em Idris. Primeiramente, introduzirei uma lista encadeada regular.

data Lista : Type -> Type where
  Vazia : Lista a
  Elem  : a -> Lista a -> Lista a

Para construir a lista [4, 5, 2] escreve-se Elem 4 (Elem 5 (Elem 2 Vazia)). Que tal fazermos uma função para extrair o primeiro elemento da lista?

cabeca : Lista a -> a
cabeca (Elem x _) = x
cabeca Vazia = ?oQueFaremosAgora

Temos um problema: alguém pode nos passar uma lista vazia, e precisamos lidar com isso de alguma forma. Um possível meio de resolver isso é lançando uma exceção. Outro meio é usar um tipo específico para possíveis valores faltando (Option a, Maybe a, etc). No entanto, quero resolver esse problema usando tipos dependentes. Antes deixe-me introduzir o tipo regular dos números naturais. É bastante simples: um número natural é ou Zero ou sucessor de outro número natural.

data Natural : Type where
  Zero : Natural
  Suc  : Natural -> Natural

Agora posso introduzir uma nova lista: uma com o tamanho especificado no seu tipo. Chama-se vetor, na literatura funcional. O vetor sempre terá esse tamanho no seu tipo, mas nem sempre conheceremos o tamanho em tempo de compilação. O que faremos é estabelecer relações entre os tipos e o tamanho.

data Vetor : Type -> Natural -> Type where
  Vazio : Vetor a Zero
  Elem  : a -> Vetor a n -> Vetor a (Suc n)

Observe que sempre que adicionamos algo ao vetor (Elem), o tamanho aumenta. Agora podemos criar nossa função para pegar o primeiro elemento do vetor.

cabeca : Vetor a (Suc n) -> a
cabeca (Elem x _) = x

Não precisamos lidar com o caso da lista vazia porque especificamos no tipo que o tamanho deve ser pelo menos 1. Suc n significa sucessor de um número n, e Zero não é sucessor de ninguém. Logo em seguida, veja aquele par ordenado dependente que foi apresentado no início do texto:

data TamVetor : Type -> Natural -> Type where
  MkTamVetor : (n : Natural) -> Vetor a n -> TamVetor a n

E uma função para extrair o tamanho, ainda que óbvia.

tamVetor : TamVetor a n -> Natural
tamVetor (MkTamVetor n _) = n

Parâmetros implícitos

Muitas linguagens com tipos dependentes têm a ideia de parâmetros implícitos de uma função. Esses parâmetros não são passados para a função na hora de executar. Eles tem o mero propósito de nos ajudarem a escrever os tipos. Além disso, costumam ser inferidos pelo compilador. É possível declará-los utilizando chaves {}, mas na maioria dos casos não é necessário. A função acima head poderia ser reescrita como:

cabeca : {a : Type} -> {n : Natural} -> Vetor a (Suc n) -> a
cabeca (Elem x _) = x

Parâmetros de Tipos vs. Índices de Tipos

Fazemos uma distinção entre parametrização e indexação de tipos. Brevemente, parâmetros de um tipo podem ser aplicados livremente, e não dizem coisa alguma sobre a forma. Podem dizer, por exemplo, o tipo do que o Vetor armazena, mas não dizem o tamanho. Enquanto isso, indíces não podem ser trocados e modelam a forma do tipo. No caso do Vetor, o Vetor era indexado pelo seu tamanho.

Podemos analisar de outra forma ainda. Vamos olhar para os construtores de Vetor (Vazio e Elem). Vamos observar como cada construtor aplica o primeiro argumento (tipo dos elementos) ao tipo Vetor. Em todos os construtores nós aplicamos um tipo genérico a, e isso não varia em momento algum. A partir disso podemos dizer que o Vetor é parametrizado pelo seu primeiro argumento.

Olhemos para o segundo argumento (o tamanho) do tipo Vetor. No construtor Vazio ele sempre é Zero. Enquanto isso, no construtor Elem nós recebemos um vetor de tamanho qualquer, e o aumentamos. O segundo argumento parece mudar de acordo com a estrutura do Vetor. Portanto o Vetor é indexado pelo tamanho.

Conclusão

Você pode não ter entendido tudo, mas não se preocupe. Atualmente, tipos dependentes ainda são uma área de pesquisa. As linguagens ainda não são amigáveis o suficiente para programadores. Costuma ser difícil programar com tipos dependentes. Ainda há muito o quê ser feito nessa área, mas tudo leva a crer que um dia serão o futuro da programação.