En matemáticas , lógica e informática , una teoría de tipos es un sistema formal en el que cada "término" tiene un "tipo". Un "tipo" en la teoría de tipos tiene un papel similar al de un "tipo" en un lenguaje de programación: dicta las operaciones que se pueden realizar en un término y, para las variables, los posibles valores por los que se puede reemplazar.
Algunas teorías de tipos sirven como alternativas a la teoría de conjuntos como fundamento de las matemáticas . Dos teorías de tipos influyentes que se propusieron como fundamentos son el cálculo λ tipado de Alonzo Church y la teoría de tipos intuicionista de Per Martin-Löf . La mayoría de los sistemas computarizados de redacción de pruebas utilizan una teoría de tipos como base. Uno común es el Cálculo de construcciones inductivas de Thierry Coquand .
La teoría de tipos está estrechamente relacionada y, en algunos casos, se superpone con los sistemas de tipos , que son una característica del lenguaje de programación utilizada para reducir errores y facilitar ciertas optimizaciones del compilador . Debido a que la teoría de tipos y los sistemas de tipos pueden superponerse, algunos expertos usan la frase "sistema de tipos" para referirse a un sistema formal específico y la frase "teoría de tipos" para referirse al estudio académico de ellos.
La teoría de tipos se creó para evitar una paradoja en una base matemática basada en la teoría de conjuntos ingenua y la lógica formal . La paradoja de Russell , que fue descubierta por Bertrand Russell , existía porque un conjunto podía definirse utilizando "todos los conjuntos posibles", que se incluían a sí mismos. Entre 1902 y 1908, Bertrand Russell propuso varias "teorías de tipos" para solucionar el problema. En 1908, Russell llegó a una teoría de tipos "ramificada" junto con un " axioma de reducibilidad ", los cuales ocuparon un lugar destacado en los Principia Mathematica de Whitehead y Russell .publicado entre 1910 y 1913. Este sistema evitó la paradoja de Russell al crear una jerarquía de tipos y luego asignar cada entidad matemática concreta (y posiblemente otra) a un tipo. Las entidades de un tipo determinado se construyen exclusivamente a partir de entidades de aquellos tipos que están más abajo en su jerarquía, evitando así que una entidad se defina utilizando a sí misma.
Los tipos no siempre se usaron en lógica. Había otras técnicas para evitar la paradoja de Russell. [1] Los tipos ganaron terreno cuando se usaron con una lógica particular, el cálculo lambda de Alonzo Church .
El ejemplo temprano más famoso es el cálculo lambda de tipo simple de Church . La teoría de tipos de Church [2] ayudó al sistema formal a evitar la paradoja de Kleene-Rosser que afectaba al cálculo lambda original sin tipos. Church demostró que podía servir como base de las matemáticas y se denominó lógica de orden superior .