Revisão das 05h01min de 6 de abril de 2005 editar 201.1.19.247 (discussão) ← Ver a alteração anterior		Revisão das 04h20min de 24 de junho de 2005 editar desfazer 200.164.231.161 (discussão) tradução de mais 3 parágrafos Ver a alteração posterior →
Linha 6: Definições de "sistemas de tipos" no contexto de linguagens de programação varia, mas a seguinte definição dada por Benjamin C. Pierce 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. ~~[A type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.~~ (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 In other words, a type system divides program values into sets called types (this is called a "type assignment"), and makes certain program behaviors illegal on the basis of the types that are thus assigned. For example, a type system may classify the value "hello" as a string and the value 5 as a number, and prohibit the programmer from adding "hello" to 5 based on that type assignment. In this type system, the program "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. ~~would be illegal. Hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers.~~ The design and implementation of type systems is a topic nearly as broad as the topic of programming languages itself. In fact, type theory proponents commonly proclaim that the design of type systems is the very essence of programming language design: "Design the type system correctly, and the language will design itself."

Teoria dos tipos: diferenças entre revisões