Tipo dependiente

Dependent type ( tipo dependiente en inglés ) en informática y lógica es un tipo que depende de algún valor. Los tipos dependientes juegan un papel clave en la teoría de tipos intuicionista y en la construcción de lenguajes de programación funcionales como ATS , Agda , Epigram e Idris .

Por ejemplo, un tipo que describe n - tuplas de números reales es dependiente porque "depende" del valor de n .

Decidir si los tipos dependientes son iguales en un programa puede requerir cálculos. Si se permiten valores arbitrarios en tipos dependientes, entonces la decisión de igualdad de tipos puede incluir verificar la igualdad del resultado del trabajo de dos programas arbitrarios. Así, la comprobación de tipos se convierte en una tarea irresoluble .

El isomorfismo de Curry-Howard le permite crear tipos para expresar propiedades matemáticas arbitrariamente complejas. Si se proporciona una prueba constructiva de que un tipo está "habitado" (es decir, hay al menos un valor de ese tipo), el compilador podrá verificar esta prueba y convertirla en un código ejecutable que evalúa el valor. La presencia de verificación de pruebas hace que los lenguajes de escritura dependiente sean similares al software de automatización de pruebas (como el probador interactivo de teoremas de Coq ).

Sistemas de cubo lambda

Henk Barendregt desarrolló el cubo lambda como un medio para clasificar los sistemas de tipos a lo largo de tres ejes. Cada una de las ocho esquinas del diagrama del cubo corresponde a un sistema tipo. En el vértice más pobre del cubo se encuentra el cálculo lambda de tipo simple , y en el vértice más rico se encuentra el cálculo de construcción . Los tres ejes del cubo corresponden a tres adiciones diferentes al cálculo lambda de tipo simple: la adición de tipos dependientes, la adición de polimorfismo y la adición de constructores de tipo de orden superior.

Formal definición

De manera muy simplificada, un tipo dependiente puede considerarse como el tipo de una familia de conjuntos indexados. Más formalmente, para un tipo (donde está el universo de tipos), puede definir una familia de tipos , que asigna cada término a un tipo , que se escribe como . Una función cuyo rango varía dependiendo de su argumento se llama función dependiente . El tipo de esta función se llama producto de tipo dependiente , tipo pi o simplemente tipo dependiente . El tipo dependiente se escribe para este caso como $A:{\mathcal {U}}$ ${\ matemáticas {U}}$ $B$ $Automóvil club británico$ $B(a):{\mathcal {U}}$ $B:A\to {\mathcal {U}}$

\Pi _{{{(x:A)}}B(x)

\Pi(x:A),B(x)

Si es una constante, entonces el tipo dependiente se simplifica a una función normal . En otras palabras, es equivalente al tipo de función . El nombre " tipo pi " enfatiza que tal tipo es un producto cartesiano de tipos. Los tipos de Pi también se pueden representar como modelos cuantificadores universales . $B$ $De la A, a la B$ $\Pi _{{{(x:A)}}B$ $De la A, a la B$

Por ejemplo, si es una tupla de números reales , entonces es el tipo de funciones que, para cualquier número natural , devuelve una tupla de números reales de tamaño . El espacio de funciones habitual es el caso especial cuando el rango no depende del parámetro de entrada: por ejemplo, - el tipo de funciones de natural a real, denotado en el cálculo lambda simplemente escrito . ${\mbox{Vec}}({{\mathbb R}},n)$ $norte$ $\Pi _{{(n:{{\mathbb N}})))}{\mbox{Vec}}({{\mathbb R}}),n)$ $norte$ $norte$ $\Pi _{{(n:{{\mathbb N}})))}\;{{\mathbb R}}$ ${{\mathbb N}}\a {{\mathbb R}}$

Las funciones polimórficas son un ejemplo importante de funciones dependientes, es decir, funciones que tienen un tipo dependiente. Para algún tipo dado, tales funciones operan sobre valores de ese tipo, o valores de un tipo derivado de ese tipo. Una función polimórfica que devuelva valores de tipotendrá un tipo polimórfico escrito como $C$

\Pi _{{(A:{\mathcal {U))))}A\a C

Literatura

Chlipala, A. Programación certificada con tipos dependientes: una introducción pragmática al asistente de prueba de Coq . - MIT Press, 2013. - 440 p. — ISBN 9780262026659 . ( texto del sitio web del autor (ing.) )
Jeremy Paul Condit. Tipos dependientes para software de sistemas seguros. — Tesis doctoral. — Universidad de California en Berkeley, 2007.