Teoria dos tipos: diferenças entre revisões

Conteúdo apagado Conteúdo adicionado
Fred Lira (discussão | contribs)
m demarcação de citação de obra
Fred Lira (discussão | contribs)
m demarcação de citação de obra
Linha 5:
Com o surgimento de poderosos [[computadores]] programáveis, e o desenvolvimento de [[linguagens de programação]] para os mesmos, Teoria dos Tipos tem encontrado aplicação prática no desenvolvimento de sistemas de tipos de linguagens de programação.
 
Definições de "sistemas de tipos" no contexto de linguagens de programação varia, mas a seguinte definição dada por Benjamin C. Pierce - dada 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."'' - (Types and Programming Languages, MIT Press, 2002).
 
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, o programa