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 funcionales como Agda , ATS , Coq , F* , Epigram , Idris y Lean , los tipos dependientes ayudan a reducir los errores al permitir al programador asignar tipos que restringen 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 retorno de una función dependiente puede depender del valor (no sólo 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 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, cuyo 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 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 capacidad de decisión de la verificación de tipos puede depender de la semántica de igualdad de la teoría de tipos dada, es decir, si la teoría de tipos es intensional o extensional . [1]
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 la lógica proposicional . Yendo más allá, para cada prueba en la lógica, había una función (término) coincidente 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 . [2]
La lógica de predicados es una extensión de la lógica proposicional, que agrega cuantificadores. Howard y de Bruijn ampliaron el cálculo lambda para que coincida con esta lógica más poderosa mediante la creación de tipos para funciones dependientes, que corresponden a "para todos", y pares dependientes, que corresponden a "existe". [3]
(Debido a este y otros trabajos de Howard, las proposiciones como tipos se conocen como la correspondencia Curry-Howard ).
En términos generales, los tipos dependientes son similares al tipo de una familia de conjuntos indexados. Más formalmente, dado un tipo en un universo de tipos , se puede tener una familia de tipos , que asigna a cada término un tipo . Decimos que el tipo B ( a ) varía con a .
Una función cuyo tipo de valor de retorno varía con su argumento (es decir, no hay un codominio fijo ) es una función dependiente y el tipo de esta función se llama tipo de producto dependiente , tipo pi ( tipo Π ) o tipo de función dependiente . [4] A partir de una familia de tipos podemos construir el tipo de funciones dependientes , cuyos términos son funciones que toman un término y devuelven un término en . Para este ejemplo, el tipo de función dependiente normalmente se escribe como o .
Si es una función constante, el tipo de producto dependiente correspondiente es equivalente a un tipo de función ordinaria . Es decir, es críticamente igual a cuando B no depende de x .
El nombre 'tipo Π' proviene de la idea de que estos pueden verse como un producto de tipos cartesiano . Los tipos Π también pueden entenderse como modelos de cuantificadores universales .
Por ejemplo, si escribimos para n -tuplas de números reales , entonces sería el tipo de función que, dado un número natural n , devuelve una tupla de números reales de tamaño n . El espacio funcional habitual surge como un caso especial cuando el tipo de rango en realidad no depende de la entrada. Por ejemplo, es el tipo de funciones desde números naturales hasta números reales, que se escribe como en el cálculo lambda mecanografiado.
Para un ejemplo más concreto, tomando A como el tipo de enteros sin signo de 0 a 255 (los que caben en 8 bits o 1 byte) y B ( a ) = X a para a : A , luego se convierte en el producto de X 0 × X 1 × X 2 × ... × X 253 × X 254 × X 255 .
El dual del tipo de producto dependiente es el tipo de par dependiente , el tipo de suma dependiente , el tipo sigma o (confusamente) el tipo de producto dependiente . [4] Los tipos sigma también pueden entenderse como cuantificadores existenciales . Siguiendo con el ejemplo anterior, si en el universo de tipos hay un tipo y una familia de tipos , entonces hay un par de tipos dependiente . (Las notaciones alternativas son similares a las de los tipos Π ).
El tipo de par dependiente captura la idea de un par ordenado donde el tipo del segundo término depende del valor del primero. Si entonces y . Si B es una función constante, entonces el tipo de par dependiente se convierte (en términos de juicio es igual a) el tipo de producto , es decir, un producto cartesiano ordinario . [4]
Para un ejemplo más concreto, tomar A nuevamente como un tipo de enteros sin signo de 0 a 255, y B ( a ) nuevamente ser igual a X a para 256 X a más arbitrarios , luego se convierte en la suma X 0 + X 1 + X 2 + ... + X 253 + X 254 + X 255 .
Sea algún tipo y deje . Según la correspondencia Curry-Howard, B puede interpretarse como un predicado lógico en términos de A. Para un dado , si el tipo B ( a ) está habitado indica si a satisface este predicado. La correspondencia puede extenderse a la cuantificación existencial y a los pares dependientes: la proposición es verdadera si y sólo si el tipo está habitado.
Por ejemplo, es menor o igual que si y sólo si existe otro número natural tal que m + k = n . En lógica, esta afirmación está codificada por cuantificación existencial:
Esta proposición corresponde al tipo de par dependiente:
Es decir, una prueba de la afirmación de que m es menor o igual que n es un par que contiene un número no negativo k , que es la diferencia entre m y n , y una prueba de la igualdad m + k = n. .
Henk Barendregt desarrolló el cubo lambda como medio para clasificar sistemas de tipos según tres ejes. Cada una de las ocho esquinas del diagrama en forma de cubo resultante corresponde a un sistema de tipos, con cálculo lambda simplemente escrito en la esquina menos expresiva y cálculo de construcciones en la más expresiva. Los tres ejes del cubo corresponden a tres aumentos diferentes del cálculo lambda de tipo simple: la adición de tipos dependientes, la adición de polimorfismo y la adición de constructores de tipos de tipo superior ( funciones de tipos a tipos, por ejemplo). El cubo lambda se generaliza aún más mediante sistemas de tipo puro .
El sistema de tipos dependientes puros de primer orden, correspondiente al marco lógico LF , se obtiene generalizando el tipo de espacio funcional del cálculo lambda simplemente tipificado al tipo de producto dependiente.
El sistema de tipos dependientes de segundo orden se obtiene permitiendo la cuantificación sobre constructores de tipos. En esta teoría, el operador del producto dependiente incluye tanto al operador del cálculo lambda simplemente escrito como al aglutinante del Sistema F.
El sistema de orden superior se extiende a las cuatro formas de abstracción del cubo lambda : funciones de términos a términos, de tipos a tipos, de términos a tipos y de tipos a términos. El sistema corresponde al cálculo de construcciones cuya derivada, el cálculo de construcciones inductivas, es el sistema subyacente del asistente de prueba de Coq .
La correspondencia Curry-Howard implica que se pueden construir tipos que expresen propiedades matemáticas arbitrariamente complejas. Si el usuario puede proporcionar una prueba constructiva de que un tipo está habitado (es decir, que existe un valor de ese tipo), entonces un compilador puede comprobar la prueba y convertirla en un código informático ejecutable que calcule el valor llevando a cabo la construcción. La función de verificación de pruebas hace que los lenguajes escritos de forma dependiente estén estrechamente relacionados con los asistentes de pruebas . El aspecto de generación de código proporciona un enfoque poderoso para la verificación formal de programas y el código portador de pruebas , ya que el código se deriva directamente de una prueba matemática verificada mecánicamente.