Teoria dos tipos

Keywords: Teoria dos tipos, Conjunto, Lógica, Matemática, Metafísica, Paradoxo de Russell, Tipo

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

[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) 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
 

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

Note that type theory, as described herein, refers to static typing disciplines. Programming systems and languages that employ dynamic typing do not prove a priori that a program uses values correctly; instead they raise an error at runtime, when the program attempts to perform some behavior that uses values incorrectly. Some claim that "dynamic typing" is a misnomer for this reason. In any case, the two should not be confused.

Major historical developments

Russell and Whitehead Lambda calculus type systems Polymorphic type inference (ML programming language; Hindley-Milner polymorphism) subtyping Object-oriented static typing (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)

Practical impact of type theory

Typed programming languages Type-driven program analysis and optimization Type-aided security mechanisms (e.g., TAL, Java bytecode verification)

Connections to constructive logic

Isomorphisms between logical proof systems and type systems Ref: Wadler's "Programs are proofs" Curry-Howard Isomorphism Intuitionistic Type Theory

Other topics we may want to add here

The notion of abstract data types The relationship between types and object-oriented programming The interplay between types and algorithms A formal definition of abstract data types - precondition, postcondition, invariants

External links:

http://www.nist.gov/dads/HTML/abstractDataType.html - Abstract data type http://www.cs.ucsd.edu/users/goguen/ps/beatcs-adj.ps.gz - A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references. Pages 3-4 appear relevant. Reference number [6] looks good, but it may not be available online.

Keywords: Teoria dos tipos, Conjunto, Lógica, Matemática, Metafísica, Paradoxo de Russell, Tipo