Tipo 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 , Clojure , Coq , F * , Epigram e Idris, los tipos dependientes ayudan a reducir los errores al permitir que el programador asigne tipos que restringen aún más el conjunto de posibles implementaciones.
Dos ejemplos comunes de tipos dependientes son funciones dependientes y pares dependientes. El tipo de retorno 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 número 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 , los cuales 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 agregan complejidad a un sistema de tipos. Decidir la igualdad de los tipos dependientes en un programa puede requerir cálculos. Si se permiten valores arbitrarios en tipos dependientes, entonces 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 usados en el cálculo lambda tipificado , y en su contraparte lógica combinatoria , seguían el mismo patrón que los axiomas en la 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 mecanografiado y la lógica intuicionista . [1]
La lógica de predicados es una extensión de la lógica proposicional, agregando cuantificadores. Howard y de Bruijn ampliaron el cálculo lambda para igualar esta lógica más poderosa creando 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 correspondencia Curry-Howard ).