tipo de dependiente
En informática y lógica , un tipo dependiente es un tipo cuya definición depende de un valor. Es una característica superpuesta de la teoría de tipos y los sistemas de tipos . En la teoría de tipos intuicionista , los tipos dependientes se utilizan para codificar cuantificadores lógicos como "para todos" y "existe". En lenguajes de programación funcional como Agda , ATS , Coq , F* , Epigram e Idris, los tipos dependientes ayudan a reducir los errores al permitir que el programador asigne tipos que restrinjan aún más el conjunto de posibles implementaciones.
Dos ejemplos comunes de tipos dependientes son las funciones dependientes y los pares dependientes. El tipo de devolución de una función dependiente puede depender del valor (no solo del tipo) de uno de sus argumentos. Por ejemplo, una función que toma un entero positivo puede devolver una matriz de longitud , donde la longitud de la matriz es parte del tipo de la matriz. (Tenga en cuenta que esto es diferente del polimorfismo y la programación genérica , que incluyen el tipo como argumento). Un par dependiente puede tener un segundo valor del cual el tipo depende del primer valor. Siguiendo con el ejemplo de la matriz, se puede usar un par dependiente para emparejar una matriz con su longitud de forma segura.
Los tipos dependientes añaden complejidad a un sistema de tipos. Decidir la igualdad de tipos dependientes en un programa puede requerir cálculos. Si se permiten valores arbitrarios en tipos dependientes, decidir la igualdad de tipos puede implicar decidir si dos programas arbitrarios producen el mismo resultado; por lo tanto , la verificación de tipos puede volverse indecidible .
En 1934, Haskell Curry notó que los tipos utilizados en el cálculo lambda tipificado , y en su contraparte de lógica combinatoria , seguían el mismo patrón que los axiomas en lógica proposicional . Yendo más allá, para cada prueba en la lógica, había una función coincidente (término) en el lenguaje de programación. Uno de los ejemplos de Curry fue la correspondencia entre el cálculo lambda simplemente tipeado y la lógica intuicionista . [1]
La lógica de predicados es una extensión de la lógica proposicional, añadiendo cuantificadores. Howard y de Bruijn ampliaron el cálculo lambda para que coincida con esta lógica más potente mediante la creación de tipos para funciones dependientes, que corresponden a "para todos", y pares dependientes, que corresponden a "existe". [2]
(Debido a este y otros trabajos de Howard, las proposiciones como tipos se conocen como la correspondencia Curry-Howard ).