Estoy interesado en obtener una comprensión realmente sólida de la escritura dependiente. He leído la mayor parte de TaPL y he leído (si no está completamente absorbido) 'Tipos dependientes' en ATTaPL . También he leído y hojeado un montón de artículos sobre mecanografía dependiente.
Muchas discusiones de teoría de tipos parecen centrarse en agregar características incrementales a los sistemas de tipos anteriores, no "¿cuál es la próxima gran generalización del sistema de tipos X?". Los tipos dependientes parecen ser la próxima gran generalización del Sistema F, pero aún no he encontrado el lenguaje intuitivo, canónico y de tipo dependiente. Las muchas referencias al cálculo de construcciones (inductivas) me hacen pensar que CoC es ese lenguaje, pero las explicaciones del lenguaje que he visto no me parecen muy claras o intuitivas.
Estoy esperando / adivinando que dicho lenguaje tendría características como: (y por favor avíseme si algo en particular resulta confuso o poco realista)
- Abstracción generalizada (puede tener funciones de cualquier dominio en la jerarquía de tipos a otra, tipo -> término, término-> tipo '' 'etc.)
- Tiene una jerarquía infinita de escritura (términos: tipos: tipos ': tipos' ': ...)
- Un número mínimo de elementos básicos. Me imagino que el lenguaje solo afirma un elemento único para cada nivel. Por ejemplo, podría afirmar que ((): Unidad: Tipo: Tipo ': ...). Otros elementos se construyen a partir de estos elementos.
- Los tipos de suma y producto son derivables.
También estoy buscando una explicación de ese lenguaje que idealmente discutiría:
- La relación entre abstracción y cuantificación en ese lenguaje. Si no están unificados, explique por qué no están unificados.
- La jerarquía de tipos infinitos explícitamente
Estoy haciendo esta pregunta porque quiero aprender la teoría del tipo dependiente, pero también porque quiero elaborar una guía que, suponiendo un poco de experiencia en CS, enseñe el uso y la comprensión de los asistentes de prueba y los idiomas mecanografiados de forma dependiente.
fuente
El cálculo que es esencialmente el núcleo de LF, a su vez, el enfoque más ampliamente reimplementado de la lógica de orden superior, es, con mucho, el sistema de tipo dependiente más simple que puede aprender, ya que consiste solo en la extensión del tipo sistema del cálculo lambda simplemente tipado con cuantificadores dependientemente tipados. Por lo tanto, las intuiciones clave necesarias para dominar LF son intuiciones que debe dominar con cualquier teoría con tipos dependientes.λπ
Twelf es un buen sistema de prueba de teoremas basado en LF. Revisando las notas avanzadas del curso ofrecidas por Frank Pfenning hay una buena introducción a la teoría y práctica de LF.
Dicho esto, tal vez no sea el mejor primer sistema para aprender si su interés está en las matemáticas constructivas en lugar de lo esencial de la teoría de tipos: LF significa marco lógico y es un sistema utilizado para axiomatizar teorías, y no se trabaja tan a menudo como Un sistema de destino directamente. El uso de un sistema basado en la teoría de tipos de Martin-Loef es probablemente la mejor introducción -Dave menciona que Agda, entre otros- es quizás un mejor punto de partida si este es su objetivo, ya que puede comenzar con los tipos aritméticos e inductivos más rápidamente en tal caso. marco de referencia.
fuente
CoC es muy probablemente el camino a seguir. Simplemente sumérgete en Coq y trabaja en un buen tutorial como Software Foundations (en el que está involucrado Pierce de TaPL y ATTaPL).
Una vez que tenga una idea de los aspectos prácticos del tipeo dependiente, vuelva a las fuentes teóricas: entonces tendrán mucho más sentido.
Su lista de características parece básicamente correcta, pero ver cómo se desarrollan en la práctica vale más que mil puntos de características.
(Otro tutorial un poco más avanzado es la programación certificada de Adam Chlipala con tipos dependientes )
fuente
Pensé que este artículo ayudó a desmitificar el concepto a nivel elemental: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html
fuente
Eche un vistazo a http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf y un sistema PiSigma anterior mencionado allí.
fuente