Teoría de Tipos Dependientes

De una familia de tipos ${\displaystyle B:A\to {\mathcal {U}}}$ podemos construir el tipo de funciones dependientes, o tipo de producto dependiente, ${\textstyle \prod _{x:A}B(x)}$ cuyos términos son funciones que toman un término ${\displaystyle a:A}$ y devuelven un término ${\displaystyle B(a)}$.

Estos tipos pueden verse como un producto cartesiano de tipos. Los tipos Π también pueden entenderse como cuantificadores universales, así que ${\textstyle \prod _{x:A}B(x)}$ puede entenderse como ${\textstyle \forall x:A.B(x)}$.

El dual del tipo de producto dependiente es el tipo de par dependiente, o de suma dependiente. Para todo tipo ${\displaystyle A:{\mathcal {U}}}$ y familia de tipos ${\displaystyle B:A\to {\mathcal {U}}}$ existe el tipo ${\textstyle \sum _{x:A}B(x)}$.

Un término de este tipo es un par (a,b) tal que ${\displaystyle a:A}$ y ${\displaystyle b:B[a/x]}$, es decir, un habitante del tipo ${\displaystyle B(x)}$ cuando sustituimos a ${\displaystyle x:A}$ por ${\displaystyle a:A}$. Estos tipos pueden entenderse también como cuantificadores existenciales tal que ${\textstyle \sum _{x:A}B(x)}$ significa ${\textstyle \exists x:A.B(x)}$.

La teoría de tipos intuicionista fue creada por Per Martin-Löf, matemático y filósofo sueco, quien la publicó por primera vez en 1975.^[2] Martin-Löf diseñó la teoría de tipos basándose en los principios del constructivismo matemático. Según este constructivismo, la verdad de una proposición depende de que tenga un "certificado" o demostración de su verdad, hecho que puede formalizarse en teoría de tipos dependientes según la Correspondencia de Curry-Howard. Una consecuencia útil es que las pruebas se convierten en objetos matemáticos que pueden examinarse, compararse y manipularse.

En esta teoría de tipos dependientes se considera además un tipo identidad para dos términos de un tipo ${\displaystyle A}$, denotado por ${\displaystyle id_{A}(a,b)}$. También tenemos el juicio metateorético: ${\displaystyle a\equiv b}$ que afirma que ambos términos son exactamente el mismo término. La identidad ${\displaystyle id_{A}(a,b)}$ no necesariamente debe interpretarse de esta forma. Por ejemplo, en el modelo homotópico de Steve Awodey y Michael Warren^[4] usado en Teoría de tipos homotópica, ${\displaystyle id_{A}(a,b)}$ se interpreta como un camino entre dos puntos de un espacio, ${\displaystyle a,b:A}$.