teoría de tipos

Generalmente, la conclusión deseada de una demostración en teoría de tipos es una de habitabilidad de tipo . ^{[ 17 ]} El problema de decisión de habitabilidad de tipo (abreviado por ⁠${\displaystyle \exists t.\Gamma \vdash t:\tau$ ?} ⁠ ) es:

Dado un contexto${\displaystyle \Gamma }$y un tipo${\displaystyle \tau }$⁠ , decidir si existe un término ⁠${\displaystyle t}$que se le puede asignar el tipo${\displaystyle \tau }$en el entorno de tipos${\displaystyle \Gamma }$⁠ .

La paradoja de Girard demuestra que la ocupación de tipos está estrechamente relacionada con la consistencia de un sistema de tipos con la correspondencia de Curry-Howard. Para ser sólido, dicho sistema debe tener tipos no ocupados.

Una teoría de tipos suele tener varias reglas, entre ellas:

• crear un juicio (conocido como contexto en este caso)
• agregar una suposición al contexto ( debilitamiento del contexto )
• reorganizar los supuestos
• usar una suposición para crear una variable
• Definir la reflexividad , la simetría y la transitividad para la igualdad de juicios.
• Definir la sustitución para la aplicación de términos lambda
• Enumera todas las interacciones de igualdad, como la sustitución.
• definir una jerarquía de universos de tipos
• afirmar la existencia de nuevos tipos

Además, para cada tipo "por regla", existen 4 tipos diferentes de reglas:

• Las reglas de "formación de tipos" indican cómo crear el tipo.
• Las reglas de "introducción de términos" definen los términos canónicos y las funciones constructoras, como "pair" y "S".
• Las reglas de "eliminación de términos" definen las otras funciones como "primero", "segundo" y "R".
• Las reglas de "cálculo" especifican cómo se realiza el cálculo con las funciones específicas de cada tipo.

Para ver ejemplos de reglas, un lector interesado puede consultar el Apéndice A.2 del libro Teoría de tipos homotópicos , ^{[ 15 ]} o leer la Teoría de tipos intuicionistas de Martin-Löf. ^{[ 18 ]}

Per Martin-Löf propuso su teoría de tipos intuicionista como fundamento de las matemáticas constructivas . ^{[ 14 ]} Las matemáticas constructivas requieren al demostrar "existe un${\displaystyle x}$con propiedad${\displaystyle P(x)}$⁠ ", uno debe construir un particular${\displaystyle x}$y una prueba de que tiene propiedad${\displaystyle P}$En la teoría de tipos, la existencia se logra utilizando el tipo de producto dependiente, y su prueba requiere un término de ese tipo.

Un ejemplo de prueba no constructiva es la prueba por contradicción . El primer paso es suponer que${\displaystyle x}$no existe y refutándolo por contradicción. La conclusión de ese paso es "no es el caso que${\displaystyle x}$no existe". El último paso es, por doble negación, concluir que${\displaystyle x}$existe. Las matemáticas constructivas no permiten el último paso de eliminar la doble negación para concluir que${\displaystyle x}$existe. ^{[ 19 ]}

La mayoría de las teorías de tipos propuestas como fundamentos son constructivas, incluyendo la mayoría de las utilizadas por los asistentes de demostración. Es posible añadir características no constructivas a una teoría de tipos, mediante reglas o suposiciones. Estas incluyen operadores sobre continuaciones, como la llamada con continuación actual . Sin embargo, estos operadores tienden a romper propiedades deseables como la canonicidad y la parametricidad .

Muchos programas que trabajan con teoría de tipos (por ejemplo, demostradores de teoremas interactivos) también realizan inferencia de tipos. Esto les permite seleccionar las reglas que el usuario pretende, con menos acciones por parte del usuario.

Aunque la motivación inicial de la teoría de categorías estaba muy alejada del fundacionalismo, ambos campos resultaron tener profundas conexiones. Como escribe John Lane Bell : «De hecho, las categorías pueden considerarse como teorías de tipos de cierto tipo; este hecho por sí solo indica que la teoría de tipos está mucho más relacionada con la teoría de categorías que con la teoría de conjuntos». En resumen, una categoría puede considerarse una teoría de tipos al considerar sus objetos como tipos (o clases ^{[ 21 ]} ), es decir, «en términos generales, una categoría puede pensarse como una teoría de tipos despojada de su sintaxis». De esta manera se derivan varios resultados significativos: ^{[ 22 ]}

• Las categorías cartesianas cerradas corresponden al cálculo λ tipificado ( Lambek , 1970);
• Los C-monoides (categorías con productos y exponenciales y un objeto no terminal) corresponden al cálculo λ no tipificado (observado independientemente por Lambek y Dana Scott alrededor de 1980);
• Las categorías cerradas cartesianas locales corresponden a teorías del tipo Martin-Löf (Seely, 1984).

Esta interacción, conocida como lógica categórica , ha sido objeto de intensa investigación desde entonces; véase, por ejemplo, la monografía de Jacobs (1999).

La teoría de tipos homotópicos intenta combinar la teoría de tipos y la teoría de categorías. Se centra en las igualdades, especialmente las igualdades entre tipos. La teoría de tipos homotópicos se diferencia de la teoría de tipos intuicionista principalmente por su tratamiento del tipo de igualdad. En 2016, se propuso la teoría de tipos cúbicos , que es una teoría de tipos homotópicos con normalización. ^{[ 23 ] [ 24 ]}

Los tipos más básicos se llaman átomos, y un término cuyo tipo es un átomo se conoce como término atómico. Los términos atómicos comunes incluidos en las teorías de tipos son los números naturales , a menudo notados con el tipo ⁠${\displaystyle {\mathsf {nat}}}$⁠ ,valores de lógica booleana ( ⁠${\displaystyle {\texttt {true}}}$y​​${\displaystyle {\texttt {false}}}$⁠ ), anotado con el tipo ⁠${\displaystyle {\mathsf {bool}}}$⁠ y variables formales , cuyo tipo puede variar. ^{[ 17 ]} Por ejemplo, los siguientes pueden ser términos atómicos.

• ${\displaystyle 42:{\mathsf {nat}}}$
• ${\displaystyle {\texttt {true}}:{\mathsf {bool}}}$
• ${\displaystyle x:{\mathsf {nat}}}$
• ${\displaystyle y:{\mathsf {bool}}}$

Además de los términos atómicos, la mayoría de las teorías de tipos modernas también permiten funciones . Los tipos de función introducen un símbolo de flecha y se definen inductivamente : Si${\displaystyle \sigma }$y${\displaystyle \tau }$son tipos, entonces la notación${\displaystyle \sigma \to \tau }$es el tipo de una función que toma un parámetro de tipo${\displaystyle \sigma }$y devuelve un término de tipo ⁠${\displaystyle \tau }$⁠ . Los tipos de esta forma se conocen como tipos simples . ^{[ 17 ]}

Algunos términos pueden declararse directamente como de tipo simple, como el siguiente término :${\displaystyle \mathrm {add} }$⁠ , que toma dos números naturales en secuencia y devuelve un número natural.

${\displaystyle \mathrm {add}$ :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})}

Estrictamente hablando, un tipo simple solo permite una entrada y una salida, por lo que una lectura más fiel del tipo anterior es que${\displaystyle \mathrm {add} }$es una función que toma un número natural y devuelve una función de la forma ⁠${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$⁠ . Los paréntesis aclaran que${\displaystyle \mathrm {add} }$no tiene el tipo${\displaystyle ({\mathsf {nat}}\to {\mathsf {nat}})\to {\mathsf {nat}}}$⁠ , que sería una función que toma como entrada una función de números naturales y devuelve un número natural. La convención es que la flecha es asociativa derecha , por lo que se pueden eliminar los paréntesis de ⁠${\displaystyle \mathrm {add} }$⁠ tipo de. ^{[ 17 ]}

Se pueden construir nuevos términos de función utilizando expresiones lambda , y se denominan términos lambda. Estos términos también se definen inductivamente: un término lambda tiene la forma ⁠${\displaystyle (\lambda v.t)}$, donde${\displaystyle v}$es una variable formal y${\displaystyle t}$es un término, y su tipo se anota ⁠${\displaystyle \sigma \to \tau }$, donde${\displaystyle \sigma }$es el tipo de${\displaystyle v}$y​${\displaystyle \tau }$es el tipo de${\displaystyle t}$⁠ . ^{[ 17 ]} El siguiente término lambda representa una función que duplica un número natural de entrada.

${\displaystyle (\lambda x.\mathrm {add} \,x\,x):{\mathsf {nat}}\to {\mathsf {nat}}}$

La variable es${\displaystyle x}$y (implícito del tipo del término lambda) debe tener tipo ⁠${\displaystyle {\mathsf {nat}}}$⁠ . El término${\displaystyle \mathrm {add} \,x\,x}$tiene tipo${\displaystyle {\mathsf {nat}}}$⁠ , lo cual se observa al aplicar dos veces la regla de inferencia de aplicación de función. Por lo tanto, el término lambda tiene tipo${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$, lo que significa que es una función que toma un número natural como argumento y devuelve un número natural.

Un término lambda es una función anónima ^{[ d ]} porque carece de nombre. El concepto de funciones anónimas aparece en muchos lenguajes de programación.

El poder de las teorías de tipos reside en especificar cómo se pueden combinar los términos mediante reglas de inferencia . ^{[ 5 ]} Las teorías de tipos que tienen funciones también tienen la regla de inferencia de aplicación de funciones : si${\displaystyle t}$es un término de tipo${\displaystyle \sigma \to \tau }$y​${\displaystyle s}$es un término de tipo${\displaystyle \sigma }$⁠ , entonces la aplicación de${\displaystyle t}$a​${\displaystyle s}$⁠ , a menudo escrito ⁠${\displaystyle (t\,s)}$⁠ , tiene tipo ⁠${\displaystyle \tau }$⁠ . Por ejemplo, si uno conoce las notaciones de tipo ⁠${\displaystyle 0:{\textsf {nat}}}$,​​${\displaystyle 1:{\textsf {nat}}}$y​​${\displaystyle 2:{\textsf {nat}}}$⁠ , entonces las siguientes notaciones de tipo se pueden deducir de la aplicación de la función. ^{[ 17 ]}

• ${\displaystyle (\mathrm {add} \,1):{\textsf {nat}}\to {\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,2)\,0):{\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,1)((\mathrm {add} \,2)\,0)):{\textsf {nat}}}$

Los paréntesis indican el orden de las operaciones ; sin embargo, por convención, la aplicación de funciones es asociativa por la izquierda , por lo que los paréntesis pueden omitirse cuando sea apropiado. ^{[ 17 ]} En el caso de los tres ejemplos anteriores, todos los paréntesis podrían omitirse de los dos primeros, y el tercero podría simplificarse a ⁠${\displaystyle \mathrm {add} \,1\,(\mathrm {add} \,2\,0):{\textsf {nat}}}$⁠ .

Las teorías de tipos que permiten términos lambda también incluyen reglas de inferencia conocidas como${\displaystyle \beta }$-reducción y${\displaystyle \eta }$-reducción. Generalizan la noción de aplicación de funciones a términos lambda. Simbólicamente, se escriben

• ${\displaystyle (\lambda v.t)\,s\rightarrow t[v\colon =s]}$( ⁠${\displaystyle \beta }$-reducción ).
• ${\displaystyle (\lambda v.t\,v)\rightarrow t}$, si${\displaystyle v}$no es una variable libre en${\displaystyle t}$( ⁠${\displaystyle \eta }$-reducción ).

La primera reducción describe cómo evaluar un término lambda: si una expresión lambda${\displaystyle (\lambda v.t)}$se aplica a un término${\displaystyle s}$⁠ , uno reemplaza cada ocurrencia de${\displaystyle v}$en${\displaystyle t}$con​${\displaystyle s}$⁠ . La segunda reducción explicita la relación entre expresiones lambda y tipos de funciones: si${\displaystyle (\lambda v.t\,v)}$es un término lambda, entonces debe ser que${\displaystyle t}$es un término de función porque se está aplicando a${\displaystyle v}$⁠ . Por lo tanto, la expresión lambda es equivalente a simplemente ⁠${\displaystyle t}$⁠ , ya que ambos toman un argumento y aplican${\displaystyle t}$a ello. ^{[ 5 ]}

Por ejemplo, el siguiente término puede ser:${\displaystyle \beta }$-reducido.

${\displaystyle (\lambda x.\mathrm {add} \,x\,x)\,2\rightarrow \mathrm {add} \,2\,2}$

En las teorías de tipos que también establecen nociones de igualdad para tipos y términos, existen reglas de inferencia correspondientes.${\displaystyle \beta }$-igualdad y${\displaystyle \eta }$-igualdad. ^{[ 17 ]}

El tipo vacío no tiene términos. El tipo generalmente se escribe${\displaystyle \bot }$o​${\displaystyle \mathbb {0} }$⁠ . Un uso para el tipo vacío son las pruebas de habitabilidad de tipos . Si para un tipo ⁠${\displaystyle a}$⁠ , es consistente derivar una función de tipo ⁠${\displaystyle a\to \bot }$, entonces${\displaystyle a}$está deshabitada , lo que quiere decir que no tiene términos.

El tipo de unidad tiene exactamente 1 término canónico. El tipo está escrito${\displaystyle \top }$o${\displaystyle \mathbb {1} }$y el único término canónico se escribe ⁠${\displaystyle \ast }$⁠ . El tipo de unidad también se utiliza en pruebas de habitabilidad de tipo. Si para un tipo ⁠${\displaystyle a}$⁠ , es consistente derivar una función de tipo ⁠${\displaystyle \top \to a}$, entonces${\displaystyle a}$está habitado , lo que significa que debe tener uno o más términos.

El tipo booleano tiene exactamente 2 términos canónicos. El tipo se suele escribir${\displaystyle {\textsf {bool}}}$o${\displaystyle \mathbb {B} }$o​${\displaystyle \mathbb {2} }$Los términos canónicos suelen ser${\displaystyle \mathrm {true} }$y​${\displaystyle \mathrm {false} }$⁠ .

Los números naturales se suelen implementar al estilo de la aritmética de Peano . Existe un término canónico.${\displaystyle 0:{\mathsf {nat}}}$para cero. Los valores canónicos mayores que cero utilizan aplicaciones iteradas de una función sucesora .${\displaystyle \mathrm {S}$ :{\mathsf {nat}}\to {\mathsf {nat}}} ⁠ .

El tipo de producto ,${\displaystyle \times }$Depende de dos tipos, y sus términos se suelen escribir como pares ordenados .${\displaystyle (s,t)}$⁠ . La pareja${\displaystyle (s,t)}$tiene el tipo de producto ⁠${\displaystyle \sigma \times \tau }$, donde${\displaystyle \sigma }$es el tipo de${\displaystyle s}$y${\displaystyle \tau }$es el tipo de${\displaystyle t}$Cada tipo de producto se define generalmente con funciones eliminadoras .${\displaystyle \mathrm {first}$ :\sigma \times \tau \to \sigma } y ⁠${\displaystyle \mathrm {second}$ :\sigma \times \tau \to \tau } ⁠ .

• ${\displaystyle \mathrm {first} \,(s,t)}$devoluciones​${\displaystyle s}$y​
• ${\displaystyle \mathrm {second} \,(s,t)}$devoluciones​${\displaystyle t}$⁠ .

Además de los pares ordenados, este tipo se utiliza para los conceptos de conjunción lógica e intersección .

El tipo de suma se escribe como${\displaystyle +}$o​${\displaystyle \sqcup }$⁠ . En los lenguajes de programación, los tipos suma pueden denominarse uniones etiquetadas . Cada tipo${\displaystyle \sigma \sqcup \tau }$generalmente se define con constructores${\displaystyle \mathrm {left}$ :\sigma \to (\sigma \sqcup \tau )} y ⁠${\displaystyle \mathrm {right}$ :\tau \to (\sigma \sqcup \tau )} ⁠ , que soninyectivas, y una función eliminadora${\displaystyle \mathrm {match}$ :(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho } tal que

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$devoluciones​${\displaystyle f\,x}$y​
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$devoluciones​${\displaystyle g\,y}$⁠ .

El tipo suma se utiliza para los conceptos de disyunción lógica y unión .

Con el polimorfismo, las funciones de eliminación se pueden definir genéricamente para todos los tipos de productos como${\displaystyle \mathrm {first}$ :\forall \,\sigma \,\tau .\sigma \times \tau \to \sigma } y ⁠${\displaystyle \mathrm {second}$ :\forall \,\sigma \,\tau .\sigma \times \tau \to \tau } ⁠ .

• ${\displaystyle \mathrm {first} \,(s,t)}$devoluciones​${\displaystyle s}$y​
• ${\displaystyle \mathrm {second} \,(s,t)}$devoluciones​${\displaystyle t}$⁠ .

Asimismo, los constructores de tipo suma se pueden definir para todos los tipos válidos de miembros suma como${\displaystyle \mathrm {left}$ :\forall \,\sigma \,\tau .\sigma \to (\sigma \sqcup \tau )} y ⁠${\displaystyle \mathrm {right}$ :\forall \,\sigma \,\tau .\tau \to (\sigma \sqcup \tau )} ⁠ , que soninyectivas, y la función eliminadora se puede dar como${\displaystyle \mathrm {match}$ :\forall \,\sigma \,\tau \,\rho .(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho } tal que

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$devoluciones​${\displaystyle f\,x}$y​
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$devoluciones​${\displaystyle g\,y}$⁠ .

Dos tipos comunes de dependencias , los tipos de producto dependiente y suma dependiente, permiten que la teoría codifique la lógica intuicionista BHK actuando como equivalentes a la cuantificación universal y existencial ; esto se formaliza mediante la correspondencia de Curry-Howard . ^{[ 26 ]} Como también se conectan con productos y sumas en la teoría de conjuntos , a menudo se escriben con los símbolos${\displaystyle \Pi }$y​${\displaystyle \Sigma }$, respectivamente.

Los tipos suma se observan en pares dependientes , donde el segundo tipo depende del valor del primer término. Esto surge de forma natural en la informática, donde las funciones pueden devolver diferentes tipos de salidas en función de la entrada. Por ejemplo, el tipo booleano se define normalmente con una función eliminadora .${\displaystyle \mathrm {if} }$, que toma tres argumentos y se comporta de la siguiente manera.

• ${\displaystyle \mathrm {if} \,{\texttt {true}}\,x\,y}$devoluciones​${\displaystyle x}$y​
• ${\displaystyle \mathrm {if} \,{\texttt {false}}\,x\,y}$devoluciones​${\displaystyle y}$⁠ .

Definiciones ordinarias de${\displaystyle \mathrm {if} }$requerir${\displaystyle x}$y${\displaystyle y}$tener el mismo tipo. Si la teoría de tipos permite tipos dependientes, entonces es posible definir un tipo dependiente.${\displaystyle x:{\mathsf {bool}}\,\vdash \,\mathrm {TF} \,x:U\to U\to U}$de tal manera que

• ${\displaystyle \mathrm {TF} \,{\texttt {true}}\,\sigma \,\tau }$devoluciones​${\displaystyle \sigma }$y​
• ${\displaystyle \mathrm {TF} \,{\texttt {false}}\,\sigma \,\tau }$devoluciones​${\displaystyle \tau }$⁠ .

El tipo de${\displaystyle \mathrm {if} }$entonces se puede escribir como ⁠${\displaystyle \forall \,\sigma \,\tau .\Pi _{x:{\mathsf {bool}}}.\sigma \to \tau \to \mathrm {TF} \,x\,\sigma \,\tau }$⁠ .

Siguiendo la noción de correspondencia de Curry-Howard, el tipo identidad es un tipo introducido para reflejar la equivalencia proposicional , en contraposición a la equivalencia de juicio (sintáctica) que ya proporciona la teoría de tipos.

Un tipo identidad requiere dos términos del mismo tipo y se escribe con el símbolo ⁠${\displaystyle =}$⁠ . Por ejemplo, si${\displaystyle x+1}$y${\displaystyle 1+x}$son términos, entonces${\displaystyle x+1=1+x}$es un tipo posible. Los términos canónicos se crean con una función de reflexividad ,${\displaystyle \mathrm {refl} }$⁠ . Por un plazo ⁠${\displaystyle t}$⁠ , la llamada${\displaystyle \mathrm {refl} \,t}$devuelve el término canónico que habita el tipo ⁠${\displaystyle t=t}$⁠ .

La complejidad de la igualdad en la teoría de tipos la convierte en un tema de investigación activo; la teoría de tipos homotópicos es un área de investigación destacada que se ocupa principalmente de la igualdad en la teoría de tipos.

Los tipos inductivos constituyen una plantilla general para crear una gran variedad de tipos. De hecho, todos los tipos descritos anteriormente, y muchos más, pueden definirse utilizando las reglas de los tipos inductivos. Dos métodos para generar tipos inductivos son la inducción-recursión y la inducción-inducción . Un método que solo utiliza términos lambda es la codificación de Scott .

Algunos asistentes de demostración , como Rocq (anteriormente conocido como Coq ) y Lean , se basan en el cálculo para construcciones inductivas, que es un cálculo de construcciones con tipos inductivos.