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 pueden ayudar a reducir 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 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 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 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 .
Historia
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 ).
Definicion formal
Π tipo
Hablando libremente, los tipos dependientes son similares al tipo de una familia de conjuntos indexados. Más formalmente, dado un tipo en un universo de tipos , uno 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, hay no se fija codomain ) es una función dependiente y el tipo de esta función se llama dependiente de tipo de producto , de tipo pi o tipo de función dependiente . [3] De una familia de tipos podemos construir el tipo de funciones dependientes , cuyos términos son funciones que toman un término y devolver un plazo en . Para este ejemplo, el tipo de función dependiente generalmente 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 juzgablemente igual a cuando B no depende de x .
El nombre 'tipo pi' proviene de la idea de que estos pueden verse como un producto cartesiano de tipos. Los tipos Pi también pueden entenderse como modelos de cuantificadores universales .
Por ejemplo, si escribimos para n -tuplas de números reales , entoncesserí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 de funciones habitual surge como un caso especial cuando el tipo de rango no depende realmente de la entrada. P.ej es el tipo de funciones desde números naturales hasta números reales, que se escribe como en cálculo lambda tipificado.
Para un ejemplo más concreto, teniendo A sea igual a la familia de enteros sin signo de 0 a 255, (las que pueden encajar en 8 bits o 1 byte) y B (a) = X una para 256 arbitraria X un 's , luegose convierte en el producto de X 0 × X 1 × X 2 × ... × X 253 × X 254 × X 255 precisamente porque el conjunto finito de enteros de 0 a 255 finalmente se detendría en los límites que se acaban de mencionar, dando como resultado una codominio de la función dependiente.
Σ tipo
El doble del tipo de producto dependiente es el tipo de par dependiente , dependiente de tipo suma , de tipo sigma , o (confusamente) dependiente de tipo de producto . [3] 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 Π).
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 luego y . Si B es una función constante, entonces el tipo de par dependiente se convierte en (es juzgablemente igual a) el tipo de producto , es decir, un producto cartesiano ordinario.
Para un ejemplo más concreto, teniendo A a de nuevo sea igual a la familia de enteros sin signo de 0 a 255, y B (a) a de nuevo sea igual a X una para 256 más arbitraria X un 's, entoncesdevuelve a la suma X 0 + X 1 + X 2 + ... + X 253 + X 254 + X 255 por las mismas razones que lo que sucedió con el codominio de la función dependiente.
Ejemplo como cuantificación existencial
Dejar ser de algún tipo, y dejar . Por la correspondencia Curry-Howard , B puede ser interpretado como una lógica de predicado en términos de A . Para una dada, si el tipo B (a) está habitado indica si a satisface este predicado. La correspondencia puede extenderse a la cuantificación existencial y los pares dependientes: la proposiciónes cierto si y solo si el tipo está habitada.
Por ejemplo, es menor o igual que si y solo si existe otro número natural tal que m + k = n . En lógica, esta afirmación está codificada por cuantificación existencial:
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 cálculo lambda simplemente mecanografiado 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 simplemente tipado: la adición de tipos dependientes, la adición de polimorfismo y la adición de constructores de tipos de kinded 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, correspondientes al marco lógico LF , se obtiene generalizando el tipo de espacio funcional del cálculo lambda simplemente tipado al tipo de producto dependiente.
Teoría de tipos dependientes de segundo orden
El sistema de tipos dependientes de segundo orden se obtiene de al permitir la cuantificación sobre constructores de tipos. En esta teoría, el operador del producto dependiente subsume tanto el operador de cálculo lambda simplemente tipado y el aglutinante de System F .
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 prueba de Coq .
Lenguaje y lógica de programación simultánea
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 verificar la prueba y convertirla en un código de computadora ejecutable que calcule el valor realizando la construcción. La función de verificación de pruebas hace que los lenguajes de escritura dependiente estén estrechamente relacionados con los asistentes de prueba . El aspecto de generación de código proporciona un enfoque poderoso para la verificación formal del programa y el código de prueba , ya que el código se deriva directamente de una prueba matemática verificada mecánicamente.
Comparación de idiomas con tipos dependientes
Idioma | Desarrollado activamente | Paradigma [nota 1] | Táctica | Condiciones de prueba | Comprobación de terminación | Los tipos pueden depender de [fn 2] | Universos | Prueba de irrelevancia | Extracción de programa | La extracción borra términos irrelevantes |
---|---|---|---|---|---|---|---|---|---|---|
Ada 2012 | Sí [4] | Imperativo | Sí [5] | Sí (opcional) [6] | ? | Cualquier término [nota 3] | ? | ? | Ada | ? |
Agda | Sí [7] | Puramente funcional | Pocas / limitadas [nota 4] | sí | Si (opcional) | Cualquier término | Sí (opcional) [fn 5] | Argumentos irrelevantes para la prueba [9] Proposiciones irrelevantes para la prueba [10] | Haskell , JavaScript | Sí [9] |
ATS | Sí [11] | Funcional / imperativo | No [12] | sí | sí | Términos estáticos [13] | ? | sí | sí | sí |
pimentón | No | Puramente funcional | No | sí | No | Cualquier término | No | No | ? | ? |
Gallina ( Coq ) | Sí [14] | Puramente funcional | sí | sí | sí | Cualquier término | Sí [nota 6] | No | Haskell , Scheme y OCaml | sí |
ML dependiente | No [nota 7] | ? | ? | sí | ? | Números naturales | ? | ? | ? | ? |
F* | Sí [15] | Funcional e imperativo | Sí [16] | sí | Si (opcional) | Cualquier término puro | sí | sí | OCaml , F # y C | sí |
Gurú | No [17] | Puramente funcional [18] | hipunión [19] | Sí [18] | sí | Cualquier término | No | sí | Carraway | sí |
Idris | Sí [20] | Puramente funcional [21] | Sí [22] | sí | Si (opcional) | Cualquier término | sí | No | sí | Sí, agresivamente [22] |
Inclinarse | sí | Puramente funcional | sí | sí | sí | Cualquier término | sí | sí | sí | sí |
Matita | Sí [23] | Puramente funcional | sí | sí | sí | Cualquier término | sí | sí | OCaml | sí |
NuPRL | sí | Puramente funcional | sí | sí | sí | Cualquier término | sí | ? | sí | ? |
PVS | sí | ? | sí | ? | ? | ? | ? | ? | ? | ? |
sabio | No [nota 8] | Puramente funcional | No | No | No | ? | No | ? | ? | ? |
Duodécimo | sí | Programación lógica | ? | sí | Si (opcional) | Cualquier término (LF) | No | No | ? | ? |
Xanadu | No [24] | Imperativo | ? | ? | ? | ? | ? | ? | ? | ? |
Ver también
- Cálculo lambda tipificado
- Teoría de tipos intuicionistas
Notas al pie
- ^ Esto se refiere allenguaje central , no a ninguna táctica ( procedimiento de demostración de teoremas) o sublenguaje de generación de código.
- ^ Sujeto a restricciones semánticas, como restricciones de universo
- ^ Static_Predicate para términos restringidos, Dynamic_Predicate para verificación similar a la afirmación de cualquier término en la conversión de tipos
- ^ Solucionador de anillos [8]
- ^ Universos opcionales, polimorfismo de universos opcionales y universos opcionales especificados explícitamente
- ^ Universos, restricciones de universo inferidas automáticamente (no lo mismo que el polimorfismo de universo de Agda) e impresión explícita opcional de restricciones de universo
- ^ Ha sido reemplazado por ATS
- ^ El último artículo de Sage y la última instantánea del código tienen fecha de 2006
Referencias
- ↑ Sørensen, Morten Heine B .; Pawel Urzyczyn (1998). "Conferencias sobre el isomorfismo de Curry-Howard". CiteSeerX 10.1.1.17.7385 . Cite journal requiere
|journal=
( ayuda ) - ^ Bove, Ana; Peter Dybjer (2008). "Tipos dependientes en el trabajo" (PDF) . Cite journal requiere
|journal=
( ayuda ) - ^ a b "ΠΣ: Tipos dependientes sin el azúcar" (PDF) .
- ^ "Página de descarga de la comunidad GNAT" .
- ^ "Predicados de subtipo RM3.2.4" .
- ^ SPARK es un subconjunto demostrable de Ada
- ^ "Página de descarga de Agda" .
- ^ "Agda Ring Solver" .
- ^ a b "Anunciar: Agda 2.2.8" . Archivado desde el original el 18 de julio de 2011 . Consultado el 28 de septiembre de 2010 .
- ^ "Registro de cambios Agda 2.6.0" .
- ^ "Descargas ATS2" .
- ^ "correo electrónico del inventor de ATS Hongwei Xi" .
- ^ "Sistema de tipo aplicado: un enfoque a la programación práctica con demostración de teoremas" (PDF) .
- ^ "Cambios de Coq en el repositorio de Subversion" .
- ^ "F * cambios en GitHub" .
- ^ "Notas de la versión F * v0.9.5.0 en GitHub" .
- ^ "Gurú SVN" .
- ^ a b 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 .
- ^ Adam Petcher (1 de abril de 2008). "Decidir las ecuaciones de base del módulo de articulación en la teoría de tipos operacionales" (PDF) . Consultado el 14 de octubre de 2010 .
- ^ "Repositorio Idris git" .
- ^ "Idris, una lengua con tipos dependientes - resumen ampliado" (PDF) . Archivado desde el original (PDF) el 16 de julio de 2011.
- ^ a b Edwin Brady. "¿Cómo se compara Idris con otros lenguajes de programación de tipo dependiente?" .
- ^ "Matita SVN" . Archivado desde el original el 8 de mayo de 2006 . Consultado el 29 de septiembre de 2010 .
- ^ "Página de inicio de Xanadu" .
Otras lecturas
- Martin-Löf, Per (1984). Teoría de tipos intuicionista (PDF) . Bibliopolis.
- Nordström, Bengt ; Petersson, Kent; Smith, Jan 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 . Publicaciones científicas de Oxford .
- 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 .
- Altenkirch, Thorsten ; McBride, Conor ; McKinna, James (abril de 2005). "Por qué son importantes los tipos dependientes" (PDF) . Cite journal requiere
|journal=
( ayuda ) - Norell, Ulf (septiembre de 2007). Hacia un lenguaje de programación práctico basado en la teoría de tipos dependientes (PDF) (PhD). Göteborg, Suecia: Departamento de Ingeniería y Ciencias de la Computación, 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.
- Norell, Ulf (2009). "Programación de tipo dependiente en Agda" (PDF) . En Koopman, P .; Plasmeijer, R .; Swierstra, D. (eds.). Programación funcional avanzada. AFP 2008 . Apuntes de conferencias en Ciencias de la Computación. 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 suave a los tipos dependientes con Idris . Publicación ajustada. ISBN 978-1723139413.
enlaces externos
- Programación de tipo dependiente 2008
- Programación de tipo dependiente 2010
- Programación de tipo dependiente 2011
- "Tipo dependiente" en la Wiki de Haskell
- teoría de tipos dependientes en nLab
- tipo dependiente en nLab
- tipo de producto dependiente en nLab
- tipo de suma dependiente en nLab
- producto dependiente en nLab
- suma dependiente en nLab