Teoria dos tipos

Básico

Teoria dos tipos é o ramo da matemática e da lógica que se preocupa com a classificação de entidades em conjuntos chamados tipos. Neste sentido, está relacionada com a noção metafísica de "tipo". A teoria dos tipos moderna foi inventada em parte em resposta ao Paradoxo de Russell, e é muito usada em Principia Mathematica, de Russell e Whitehead.

Com o surgimento de poderosos computadores programáveis, e o desenvolvimento de linguagens de programação para os mesmos, a Teoria dos Tipos tem encontrado aplicação prática no desenvolvimento de sistemas de tipos de linguagens de programação.

Definição:

a Definições de "sistemas de tipos" no contexto de linguagens de programação variam, mas a seguinte definição dada por Benjamin C. Pierce - na obra Types and Programming Languages, MIT Press, 2002 - corresponde, aproximadamente, ao consenso corrente na comunidade de Teoria dos Tipos:

"Um sistema de tipos é um método sintático tratável para provar a isenção de certos comportamentos
em um programa através da classificação de frases de acordo com as espécies de valores que elas computam."

Em outras palavras, um sistema de tipos divide os valores de um programa em conjuntos chamados tipos (isso é o que é denominado uma "atribuição de tipos"), e torna certos comportamentos do programa ilegais com base nos tipos que são atribuídos neste processo. Por exemplo, um sistema de tipos pode classificar o valor "hello" como uma cadeia de caracteres e o valor 5 como um número, e proibir o programador de tentar adicionar "hello" a 5, com base nessa atribuição de tipos. Neste sistema de tipos, a instrução

"hello" + 5

seria ilegal. Assim, qualquer programa permitido pelo sistema de tipos seria demonstravelmente livre do comportamento errôneo de tentar adicionar cadeias de caracteres a números.

O projeto e a implantação de sistemas de tipos é um tópico quase tão vasto quanto o das próprias linguagens de programação. De fato, os proponentes da Teoria dos Tipos argumentam que o projeto de sistemas de tipos é a própria essência do projeto de linguagens de programação: "Projete o sistema de tipos corretamente, e a linguagem vai projetar a si mesma".

Note que teoria dos tipos, como descrita daqui para frente, se refere a disciplinas de tipagem estática.

Sistemas de programação que aplicam tipagem dinâmica não provam a priori que um programa usa valores corretamente; ao invés disso, elas lançam um erro em tempo de execução quando o programa tenta apresentar algum comportamento que use valores incorretamente. Alguns argumentam que "tipagem dinâmica" é uma terminologia ruim por isso. De qualquer forma, as duas não devem ser confundidas.

Principais desenvolvedores

Russell e Whitehead
Sistema de cálculo de tipo Lambda (e.g Haskell)
Inferência de Tipo Polimórfica (Linguagem de Programação ML; Polimorfismo de Hindley-Milner) subtipo
Tipagem estática orientada a objetos (grew out of abstract data type and subtyping)
F-bounded polimorfismos e esforços para combinar generics com polimorfismo de orientação a objetos
Set-constraint-based type systems
Sistemas Modulares
Sistemas Baseados em Provas de Tipos (e.g. ELF)
… (muito mais)

Impacto prático da teoria dos tipos

Linguagem de programação fortemente tipadas
Análise e otimização de programas orientadas a tipos
Mecanismos de verificação de segurança de tipos e.g., TAL, verificação de bytecode do Java)

Conexões com lógica construtivista

Isomorfismos entre sistemas de provas lógicas e sistemas de tipos Ref: Wadler's "Programs are proofs" Curry-Howard Isomorphism Intuitionistic Type Theory

Outros tópicos:

A noção de tipos de dados abstratos
A relação entre tipos e programação orientada a objeto
A relação entre tipos e algoritmos
Uma definição formal de tipos de dados abstratos - pré condição, pós condição e invariantes

Ligações externas

http://www.nist.gov/dads/HTML/abstractDataType.html - Abstract (em inglês)
http://www.cs.ucsd.edu/users/goguen/ps/beatcs-adj.ps.gz - Um paper sobre o básico de ADTs, e uma boa lista de referencias. As pages 3–4 são as mais relevantes. (arquivo compactado)