# 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:
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
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