Tipo dependiente

Tipo cuya definición depende de un valor

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 , Idris y Lean , los tipos dependientes ayudan a reducir 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 las funciones dependientes y los 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 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, cuyo tipo depende del primer valor. Siguiendo con el ejemplo de la matriz, un par dependiente se puede utilizar para emparejar una matriz con su longitud de una manera segura para los tipos. ${\displaystyle n}$ ${\displaystyle n}$

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 los tipos dependientes, entonces decidir la igualdad de tipos puede implicar decidir si dos programas arbitrarios producen el mismo resultado; por lo tanto, la decidibilidad 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]

Historia

En 1934, Haskell Curry se dio cuenta de que los tipos utilizados en el cálculo lambda tipado 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) correspondiente en el lenguaje de programación. Uno de los ejemplos de Curry fue la correspondencia entre el cálculo lambda tipado simple y la lógica intuicionista . ^[2]

La lógica de predicados es una extensión de la lógica proposicional, que añade cuantificadores. Howard y de Bruijn ampliaron el cálculo lambda para que coincidiera con esta lógica más potente creando tipos para funciones dependientes, que corresponden a "para todos", y pares dependientes, que corresponden a "existe". ^[3]

Debido a esto y a otros trabajos de Howard, las proposiciones como tipos se conocen como la correspondencia Curry-Howard .

Definición formal

En términos generales, los tipos dependientes son similares al tipo de una familia indexada de conjuntos. 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 varía con . ${\displaystyle A:{\mathcal {U}}}$ ${\displaystyle {\mathcal {U}}}$ ${\displaystyle B:A\to {\mathcal {U}}}$ ${\displaystyle a:A}$ ${\displaystyle B(a):{\mathcal {U}}}$ ${\displaystyle B(a)}$ ${\displaystyle a}$

Tipo Π

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 se escribe típicamente como o . ${\displaystyle B:A\to {\mathcal {U}}}$ ${\textstyle \prod _{x:A}B(x)}$ ${\displaystyle a:A}$ ${\displaystyle B(a)}$ ${\textstyle \prod _{x:A}B(x)}$ ${\textstyle \prod {(x:A)}B(x)}$

Si es una función constante, el tipo de producto dependiente correspondiente es equivalente a un tipo de función ordinaria . Es decir, es igual en términos de juicio a cuando no depende de . ${\displaystyle B:A\to {\mathcal {U}}}$ ${\textstyle \prod _{x:A}B}$ ${\displaystyle A\to B}$ ${\displaystyle B}$ ${\displaystyle x}$

El nombre "Π-tipo" proviene de la idea de que estos pueden verse como un producto cartesiano de tipos. 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 una función que, dado un número natural n , devuelve una tupla de números reales de tamaño n . El espacio de funciones 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 tipado. ${\displaystyle \operatorname {Vec} (\mathbb {R} ,n)}$ ${\textstyle \prod _{n:\mathbb {N} }\operatorname {Vec} (\mathbb {R} ,n)}$ ${\textstyle \prod _{n:\mathbb {N} }{\mathbb {R} }}$ ${\displaystyle \mathbb {N} \to \mathbb {R} }$

Para un ejemplo más concreto, tomando como el tipo de números enteros sin signo de 0 a 255 (los que caben en 8 bits o 1 byte) y para , entonces se convierte en el producto de . ${\displaystyle A}$ ${\displaystyle B(a)=X_{a}}$ ${\displaystyle a:A}$ ${\textstyle \prod _{x:A}B(x)}$ ${\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}$

Tipo Σ

El dual del tipo de producto dependiente es el tipo de par dependiente , tipo de suma dependiente , tipo sigma o (confusamente) tipo de producto dependiente . ^[4] Los tipos sigma también pueden entenderse como cuantificadores existenciales . Continuando con el ejemplo anterior, si, en el universo de tipos , hay un tipo y una familia de tipos , entonces hay un tipo de par dependiente . (Las notaciones alternativas son similares a las de los tipos Π ). ${\displaystyle {\mathcal {U}}}$ ${\displaystyle A:{\mathcal {U}}}$ ${\displaystyle B:A\to {\mathcal {U}}}$ ${\textstyle \sum _{x:A}B(x)}$

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 es una función constante, entonces el tipo de par dependiente se convierte en (es juzgadamente igual a) el tipo de producto , es decir, un producto cartesiano ordinario . ^[4] ${\textstyle (a,b):\sum _{x:A}B(x),}$ ${\displaystyle a:A}$ ${\displaystyle b:B(a)}$ ${\displaystyle B}$ ${\displaystyle A\times B}$

Para un ejemplo más concreto, tomando nuevamente como tipo de enteros sin signo de 0 a 255, y nuevamente como igual a para 256 más arbitrario , entonces se convierte en la suma . ${\displaystyle A}$ ${\displaystyle B(a)}$ ${\displaystyle X_{a}}$ ${\displaystyle X_{a}}$ ${\textstyle \sum _{x:A}B(x)}$ ${\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}$

El ejemplo como cuantificación existencial

Sea algún tipo, y sea . Por la correspondencia Curry-Howard, puede interpretarse como un predicado lógico en términos de . Para un dado , si el tipo está habitado indica si satisface este predicado. La correspondencia puede extenderse a la cuantificación existencial y a los pares dependientes: la proposición es verdadera si y solo si el tipo está habitado. ${\displaystyle A:{\mathcal {U}}}$ ${\displaystyle B:A\to {\mathcal {U}}}$ ${\displaystyle B}$ ${\displaystyle A}$ ${\displaystyle a:A}$ ${\displaystyle B(a)}$ ${\displaystyle a}$ ${\displaystyle \exists {a}{\in }A\,B(a)}$ ${\textstyle \sum _{a:A}B(a)}$

Por ejemplo, es menor o igual a si y solo si existe otro número natural tal que . En lógica, esta afirmación está codificada por la cuantificación existencial: ${\displaystyle m:\mathbb {N} }$ ${\displaystyle n:\mathbb {N} }$ ${\displaystyle k:\mathbb {N} }$ ${\displaystyle m+k=n}$

$${\displaystyle m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.}$$

Esta proposición corresponde al tipo de par dependiente:

$${\displaystyle \sum _{k:\mathbb {N} }m+k=n.}$$

Es decir, una prueba de la afirmación de que es menor o igual a es un par que contiene tanto un número no negativo , que es la diferencia entre y , como una prueba de la igualdad . ${\displaystyle m}$ ${\displaystyle n}$ ${\displaystyle k}$ ${\displaystyle m}$ ${\displaystyle n}$ ${\displaystyle m+k=n}$

Sistemas del cubo lambda

Henk Barendregt desarrolló el cubo lambda como un medio para clasificar los sistemas de tipos a lo largo de tres ejes. Las ocho esquinas del diagrama en forma de cubo resultante corresponden cada una a un sistema de tipos, con el cálculo lambda de tipos simples en la esquina menos expresiva y el cálculo de construcciones en la más expresiva. Los tres ejes del cubo corresponden a tres ampliaciones diferentes del cálculo lambda de tipos simples: la adición de tipos dependientes, la adición de polimorfismo y la adición de constructores de tipos de clase superior (funciones de tipos a tipos, por ejemplo). El cubo lambda se generaliza aún más mediante sistemas de tipos puros .

Teoría de tipos dependientes de primer orden

El sistema de tipos dependientes puros de primer orden, correspondiente al marco lógico LF , se obtiene generalizando el tipo de espacio de funciones del cálculo lambda simplemente tipado al tipo de producto dependiente. ${\displaystyle \lambda \Pi }$

Teoría de tipos dependientes de segundo orden

El sistema de tipos dependientes de segundo orden se obtiene al permitir la cuantificación sobre los constructores de tipos. En esta teoría, el operador de producto dependiente subsume tanto el operador del cálculo lambda de tipo simple como el operador de enlace del Sistema F. ${\displaystyle \lambda \Pi 2}$ ${\displaystyle \lambda \Pi }$ ${\displaystyle \to }$ ${\displaystyle \forall }$

Cálculo lambda polimórfico de tipo dependiente de orden superior

El sistema de orden superior se extiende a las cuatro formas de abstracción del cubo lambda : funciones de términos a términos, tipos a tipos, términos a tipos y 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 demostración Coq . ${\displaystyle \lambda \Pi \omega }$ ${\displaystyle \lambda \Pi 2}$

Lenguaje de programación y lógica simultáneas

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 código informático ejecutable que calcula el valor llevando a cabo la construcción. La característica de comprobación de pruebas hace que los lenguajes con tipado 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.

Comparación de lenguajes con tipos dependientes

1. Esto se refiere al lenguaje central , no a ninguna táctica ( procedimiento de demostración de teoremas ) o sublenguaje de generación de código.
2. Sujeto a restricciones semánticas, como las restricciones del universo.
3. Static_Predicate para términos restringidos, Dynamic_Predicate para verificación tipo Assert de cualquier término en la conversión de tipo
4. Solucionador de anillos ^[8]
5. Universos opcionales, polimorfismo de universos opcionales y universos opcionales especificados explícitamente
6. Universos, restricciones de universo inferidas automáticamente (no es lo mismo que el polimorfismo del universo de Agda) e impresión explícita opcional de las restricciones del universo
7. Ha sido reemplazado por ATS
8. El último artículo de Sage y la última instantánea de código datan de 2006
9. Static_Predicate para términos restringidos, Dynamic_Predicate para verificación tipo Assert de cualquier término en la conversión de tipo

Véase también

• Cálculo lambda tipificado
• Teoría de tipos intuicionista

Referencias

1. Hofmann, Martin (1995), Conceptos extensionales en la teoría de tipos intensionales (PDF)
2. Sørensen, Morten Heine B.; Urzyczyn, Pawel (1998), Conferencias sobre el isomorfismo de Curry-Howard , CiteSeerX 10.1.1.17.7385 
3. Bove, Ana; Dybjer, Peter (2008). Tipos dependientes en el trabajo (PDF) (Informe). Universidad Tecnológica de Chalmers.
4. Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas (2010). "ΠΣ: Dependent Types without the Sugar" (PDF) . En Blume, Matthias; Kobayashi, Naoki; Vidal, Germán (eds.). Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japón, 19-21 de abril de 2010. Actas . Lecture Notes in Computer Science. Vol. 6009. Springer. págs. 40–55. doi :10.1007/978-3-642-12251-4_5.
5. "Instalación de GNAT Ada usando ALIRE".
6. "§3.2.4 Predicados de subtipo". Manual de referencia de Ada (edición de 2012).
7. "Página de descarga de Agda".
8. "Solucionador de anillos de Agda".
9. "Anuncio: Agda 2.2.8". Archivado desde el original el 18 de julio de 2011. Consultado el 28 de septiembre de 2010 .
10. "Registro de cambios de Agda 2.6.0".
11. "Descargas ATS2".
12. "correo electrónico del inventor de ATS, Hongwei Xi".
13. Xi, Hongwei (marzo de 2017). "Sistema de tipos aplicado: un enfoque para la programación práctica con demostración de teoremas" (PDF) . arXiv : 1703.08683 .
14. "Cambios de Coq en el repositorio de Subversion".
15. "Introducción de SProp en Coq 8.10".
16. "F* cambios en GitHub". GitHub .
17. "Notas de la versión F* v0.9.5.0 en GitHub". GitHub .
18. "Gurú SVN".
19. Aaron Stump (6 de abril de 2009). "Programación verificada en Guru" (PDF) . Archivado desde el original (PDF) el 29 de diciembre de 2009. Consultado el 28 de septiembre de 2010 .
20. Petcher, Adam (mayo de 2008). Decidir la capacidad de unión módulo ecuaciones fundamentales en la teoría de tipos operacionales (PDF) (MSc). Washington University . Consultado el 14 de octubre de 2010 .
21. "Repositorio Git de Idris". GitHub . 17 de mayo de 2022.
22. Brady, Edwin. "Idris, un lenguaje con tipos dependientes: resumen extendido" (PDF) . CiteSeerX 10.1.1.150.9442 . 
23. Brady, Edwin. "¿En qué se diferencia Idris de otros lenguajes de programación con tipos dependientes?".
24. "Matita SVN". Archivado desde el original el 8 de mayo de 2006. Consultado el 29 de septiembre de 2010 .
25. "Instalación de SPARK utilizando ALIRE".
26. "§3.2.4 Predicados de subtipo". Manual de referencia de Ada (edición de 2012).
27. "5.11.6. Biblioteca de lemas SPARK". Guía del usuario de SPARK (25.0 ed.).
28. "5.2.8. Contratos de rescisión". Guía del usuario de SPARK (25.0 ed.).
29. "1.2. Llamada y uso de CCG". Suplemento de la Guía del usuario del generador de código común de GNAT Pro (edición 25.0).
30. "Compilar con un compilador que no sea compatible con SPARK". Guía del usuario de SPARK (edición 25.0).

Lectura adicional

• Martin-Löf, Per (1984). Teoría de tipos intuicionista (PDF) . Bibliopolis.
• Nordström, Bengt; Petersson, Kent; Smith, enero M. (1990). Programación en la teoría de tipos de Martin-Löf: una introducción. Prensa de la Universidad de Oxford. ISBN 9780198538141.
• Barendregt, H. (1992). "Cálculos lambda con tipos". En Abramsky, S.; Gabbay, D.; Maibaum, T. (eds.). Manual de lógica en informática . Oxford Science Publications . doi :10.1017/CBO9781139032636. hdl : 2066/17231 .
• Brandl, Helmut (2022). Cálculo de construcciones
• McBride, Conor ; McKinna, James (enero de 2004). "La vista desde la izquierda". Revista de programación funcional . 14 (1): 69–111. doi : 10.1017/s0956796803004829 . S2CID  6232997.
• Altenkirch, Thorsten ; McBride, Conor ; McKinna, James (2006). "Por qué son importantes los tipos dependientes" (PDF) . Actas del 33.º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación, POPL 2006, Charleston, Carolina del Sur, EE. UU., 11-13 de enero . ISBN 1-59593-027-2.
• Norell, Ulf (septiembre de 2007). Towards a practical programming language based on dependent type theory (PDF) (PhD). Gotemburgo, Suecia: Departamento de Ciencias Informáticas e Ingeniería, Universidad Tecnológica de Chalmers. ISBN 978-91-7291-996-9.
• Oury, Nicolas; Swierstra, Wouter (2008). "El poder de Pi" (PDF) . ICFP '08: Actas de la 13.ª conferencia internacional ACM SIGPLAN sobre programación funcional . págs. 39-50. doi :10.1145/1411204.1411213. ISBN. 9781595939197. Número de identificación del sujeto  16176901.
• Norell, Ulf (2009). "Programación escrita de forma dependiente en Agda" (PDF) . En Koopman, P.; Plasmeijer, R.; Swierstra, D. (eds.). Programación funcional avanzada. AFP 2008 . Apuntes de conferencias sobre informática. vol. 5832. Saltador. págs. 230–266. doi :10.1007/978-3-642-04652-0_5. ISBN 978-3-642-04651-3.
• Sitnikovski, Boro (2018). Introducción sencilla a los tipos dependientes con Idris . Lean Publishing. ISBN 978-1723139413.
• McBride, Conor ; Nordvall-Forsberg, Fredrik (2022). "Sistemas de tipos para programas que respetan las dimensiones" (PDF) . Herramientas matemáticas y computacionales avanzadas en metrología y pruebas XII . Avances en matemáticas para ciencias aplicadas. World Scientific. págs. 331–345. doi :10.1142/9789811242380_0020. ISBN 9789811242380. Número de identificación del sujeto  243831207.

Enlaces externos

• Programación de tipos dependientes 2008
• Programación de tipos dependientes 2010
• Programación de tipos dependientes 2011
• "Tipo dependiente" en la Wiki de Haskell
• Teoría de tipos dependientes en el laboratorio n
• tipo dependiente en el laboratorio n
• Tipo de producto dependiente en el laboratorio n
• Tipo de suma dependiente en el laboratorio n
• producto dependiente en el laboratorio n
• suma dependiente en el n Lab