 | Este artigonão citafontes confiáveis. Ajude ainserir referências. Conteúdo nãoverificável pode ser removido.—Encontre fontes:Google (N • L • A • I • WP refs) • ABW • CAPES(dezembro de 2013) |
Teoria dos tipos é o ramo damatemática e dalógica que se preocupa com a classificação de entidades emconjuntos chamadostipos. Neste sentido, está relacionada com a noçãometafísica de "tipo". A teoria dos tipos moderna foi inventada em parte em resposta aoParadoxo de Russell, e é muito usada emPrincipia Mathematica, deRussell eWhitehead.
Com o surgimento de poderososcomputadores programáveis, e o desenvolvimento delinguagens de programação para os mesmos, a Teoria dos Tipos tem encontrado aplicação prática no desenvolvimento de sistemas de tipos delinguagens de programaçã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 obraTypes 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 comportamentosem 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 detipagem estática.
Sistemas de programação que aplicamtipagem dinâmica não provam a priori que um programa usa valores corretamente; ao invés disso, elas lançam um erro emtempo 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.
Conexões com lógica construtivista
Isomorfismos entre sistemas de provas lógicas e sistemas de tiposRef: Wadler's "Programs are proofs"Curry-Howard IsomorphismIntuitionistic Type Theory
