Quiero entender la teoría de tipos, pero primero tengo que saber cómo puedo aplicarla. ¿Podría haber más aplicaciones no obvias de la teoría de tipos aparte de los sistemas de tipos en programación? ¿Podría haber otras aplicaciones, digamos en el perfil de personalidad y los gustos?
type-theory
applied-theory
Tamad Lang
fuente
fuente
Respuestas:
Puede interesarle el trabajo sobre Ceptre , resultado de la investigación de doctorado de Chris Martens , que utiliza la teoría de tipos para la narración interactiva. A continuación se cita el resumen de la tesis :
fuente
Ha habido usos interesantes de la teoría de tipos en lingüística. Véanse, por ejemplo, las obras lingüísticas de Chung-chieh Shan o Christian Rétoré .
A continuación se cita la descripción del libro de Rétoré sobre gramáticas categoriales:
La siguiente cita se encuentra en la introducción del capítulo del libro de Efectos secundarios lingüísticos de Shan :
fuente
Debido a la correspondencia de Curry-Howard , los tipos pueden interpretarse como proposiciones y las proposiciones como tipos.
Como resultado de esto, la teoría de tipos es aplicable literalmente a cualquier campo que use lógica formal para sus pruebas. Esto puede ser verificación de circuito, análisis real, lógica simbólica, geometría, etc.
Por ejemplo, algunas herramientas de verificación de pruebas automatizadas funcionan utilizando este principio: verifican la validez de la prueba al verificar un término en particular en algún sistema de tipos. El comprobador de pruebas LF se basa en este enfoque, al igual que HOL Light . Como aplicación de ejemplo, el código de transporte de pruebas utilizó LF para verificar las pruebas de seguridad de memoria de código no confiable. El beneficio de usar este tipo de comprobador de pruebas es que la implementación puede ser muy simple y, por lo tanto, podemos asegurarnos de que la implementación sea correcta. Ver, por ejemplo, el siguiente documento:
Damas de prueba fundacional con pequeños testigos . Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.
fuente
Un artículo interesante que explica las aplicaciones de los tipos dependientes es The Power of Pi , que muestra cómo Agda puede usarse para resolver problemas interesantes.
Otro buen ejemplo es el uso de tipos dependientes para el control de recursos. Un buen ejemplo es la API de gestión de archivos de Efectos de Idris . Por ejemplo, la función para leer una línea de un archivo tiene el siguiente tipo
que especifica que esta función solo es aplicable si hay un archivo abierto. La lista entre llaves indica qué efectos están disponibles. En este caso, tenemos que esta función requiere el efecto de tener un archivo abierto para leer.
Puede encontrar más información sobre la biblioteca de efectos aquí .
Una aplicación más es el uso de tipos dependientes para la concurrencia como se informa en el siguiente artículo por el creador de Idris.
fuente
como se menciona en la respuesta de jmite, la lógica de orden superior / teoría de tipos en la verificación de circuitos / hardware / electrónica ha existido durante décadas y ahora es tan rutinaria que ni siquiera se percibe / considera tanto como una "aplicación" después de un esfuerzo de transferencia aparentemente importante en la década de 1990 aunque todavía es un área activa de investigación También hay mucha aplicación de Coq y su lógica de tipo, en particular para la verificación de circuitos / hardware / electrónica desde la lógica de compuerta de bajo nivel hasta estructuras / subsistemas de nivel / orden mucho más altos. aquí hay algunas referencias clave
Lógica de orden superior y verificación de hardware / Melham (1993!)
Prueba de teorema lógico de orden superior y sus aplicaciones / Claeson, Gordon
Construcción de circuitos correctos: verificación de aspectos funcionales de las especificaciones de hardware con tipos dependientes / Brady, Mckinna, Hammond
Certificación de circuitos en Teoría de tipo / Grimal
Coquet: una biblioteca de Coq para verificar hardware / Braibant
fuente