En ciencia de la computación específicamente, la teoría de tipos constructivos hace una aparición completa en los lenguajes centrales de los probadores de teoremas mecanizados. Para ser un poco más específico, la teoría de tipos constructivos hace una aparición directa en los lenguajes centrales de los sistemas de desarrollo de pruebas como Coq, Agda, Lean, NuPRL y Twelf. Más allá de su completa aparición en los lenguajes centrales de los demostradores de teoremas mecanizados, la teoría de tipos constructivos también ha influido en el diseño de lenguajes de programación concretos para escribir programas ejecutables, particularmente en la familia ML. Por ejemplo, el sistema formal F-omega se puede ver como una versión restringida de la teoría de tipos constructivos donde hay una distinción explícita entre términos y tipos ; El sistema formal F-omega aparece en los lenguajes centrales de los lenguajes de programación como Standard ML, Haskell y PureScript. Estos lenguajes de programación se basan en una distinción explícita entre términos y tipos en sus lenguajes principales, es decir, para que los tipos puedan borrarse durante la compilación, y para que sea más fácil separar el diseño de la estática del lenguaje del de la dinámica de idioma. Quizás en un grado ligeramente menor, la teoría de tipos constructivos también ha influido en el diseño de lenguajes de programación como Rust y Scala. Es discutible que la teoría de tipos constructivos, al menos basada en cómo se originó históricamente, haya tenido menos influencia en el diseño de lenguajes de programación concretos fuera de la familia ML.
También hay una aplicación de lo que se conoce como teoría de tipo lineal que encuentro muy interesante, que he encontrado recientemente. En resumen, la teoría del tipo lineal puede pensarse en una variante de la teoría del tipo constructivo donde las hipótesis son por defecto recursos en lugar de hechos , por lo que por defecto no se pueden duplicar más de una vez cuando se usan para probar o, en otras palabras, lograr Un objetivo particular. Recientemente me he encontrado con una implementación de un marco lógico basado en la teoría de tipo lineal; Las pruebas en un marco lógico se construyen sobre la base de derivaciones lógicas directas de un conjunto de constantes, suposiciones iniciales y un conjunto de reglas, a diferencia del tipo de pruebas inductivas que se verifican para verificar su admisibilidad en sistemas de desarrollo de pruebas como Coq o Agda. El autor de dicho marco lógico, Chris Martens, está aplicando la teoría de tipo lineal a la narración interactiva y la generación narrativa, lo que me parece bastante interesante. Por ejemplo, es posible modelar una tragedia de Shakespeare en dicho marco lógico, y usar el soporte del marco lógico para la búsqueda de pruebas automatizadas para generar posibles historias de cómo la obra podría terminar en una tragedia a partir de condiciones iniciales particulares. Aquí está el enlace a dicho proyecto. Personalmente, me parece muy emocionante cómo la teoría de tipos también puede tener aplicaciones como esta en informática.
Alejándose un poco de la informática, también hay algunas aplicaciones de la teoría de tipos en lingüística computacional, que también me parecen muy interesantes. Por ejemplo, recientemente Jon Sterling y Darryl McAdams han aplicado la teoría de tipos para modelar la unión de pronombres y la resolución de presupuestos en Tipos dependientes para la pragmática . Continuando con esta línea de trabajo se encuentra la conferencia de Jon sobre Oráculos y secuencias de elección para la pragmática teórica tipo , y el proyecto de Darryl, The Language Engine . También está el Marco Gramatical , que aparentemente se ha utilizado para estudiar: la sintaxis formal del griego antiguo, la interacción humano-computadora basada en el idioma y los sistemas de traducción multilingüe, por nombrar algunos ejemplos. En general, no estoy muy familiarizado con las aplicaciones de la teoría de tipos a la lingüística computacional; Sin embargo, me parece bastante emocionante que haya potencial para que la teoría de tipos se aplique también a la lingüística de compilación.
- ¿Qué se puede hacer en una computadora sin conexión a Internet?
- ¿Cómo utiliza la informática el método científico?
- En teoría, ¿podría una máquina Turing de inteligencia sobrehumana no ser un desarrollo de un solo hombre? ¿Podría ser construido solo por varias personas juntas?
- Informática: ¿Cuál es un buen libro de algoritmos / CS para leer mientras viaja?
- ¿Cuál es el mejor camino a seguir como estudiante de primer año para ingresar a la especialidad de CS?
