Ipc_teoria Dos Tipos

teoria dos tipos origem: wikip�dia, a enciclop�dia livre. (redirecionado de teoria dos tipos) ir para: navega��o, pesquisa este artigo encontra-se parcialmente em l�ngua estrangeira. ajude e colabore com a tradu��o. no sentido mais lato, a 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, 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 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

"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 pra 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

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 polymorphism and efforts to combine generic w/ oo polymorphism set-constraint-based type systems module systems type-driven proof systems (e.g. elf) ... (much more) impacto pr�tico da teoria dos tipos linguagem de programa��o fortemente tipadas type-driven program analysis and optimization type-aided security mechanisms (e.g., tal, java bytecode verification) conex�es com l�gica construtivista isomorphisms between logical proof systems and type systems ref: wadler's "programs are proofs" curry-howard isomorphism intuitionistic type theory outros t�picos que podemos querer adicionar aqui a no��o de tipos de dados abstratos a rela��o entre tipos e programa��o orientada a objeto the interplay between types and algorithms uma defini��o formal de tipos de dados abstratos - pr�-codi��o, p�s-condi��o e invariantes

[editar] liga��es externas