¿Qué es Haskell''s Data.Typeable?
typeclass generic-programming (4)
Es una biblioteca que permite, entre otras cosas, nombrar tipos. Si un tipo a se declara Typeable , puede obtener su nombre usando show $ typeOf x donde x es cualquier valor de tipo a . También presenta un tipo de fundición limitado .
(Esto es algo similar al RTTI de C ++ o al reflejo de los lenguajes dinámicos).
He encontrado referencias a Haskell''s Data.Typeable . Data.Typeable , pero no tengo claro por qué querría usarlo en mi código.
¿Qué problema soluciona y cómo?
La clase Data.Typeable se usa principalmente para programación genérica en el estilo Scrap Your Boilerplate (SYB). Ver también Data.Data
La idea es que SYB defina una combinación de recolectores para realizar operaciones tales como impresión, conteo, búsqueda, sustitución, etc. de manera uniforme en una variedad de tipos creados por el usuario. La Typeable Typeable proporciona la fontanería necesaria.
En GHC moderno, puede decir deriving Data.Typeable al definir su propio tipo para proporcionarle las instancias necesarias.
Una de las primeras descripciones que pude encontrar de una biblioteca similar a Data.Typeable para Haskell es la de John Peterson de 1992: http://www.cs.yale.edu/publications/techreports/tr1022.pdf
El primer documento "oficial" que conozco sobre la introducción de la biblioteca Data.Typeable es el primer documento Scrap Your Boilerplate de 2003: http://research.microsoft.com/en-us/um/people/simonpj/Papers/hmap/index.htm
¡Estoy seguro de que hay mucha historia intermedia con la que alguien puede hablar!
Data.Typeable es una codificación de un enfoque bien conocido (véase, por ejemplo, Harper) para implementar la verificación de tipo demorada (dinámica) en un lenguaje de tipo estático, utilizando un tipo universal .
Dicho tipo ajusta el código para el cual la verificación de tipos no tendría éxito hasta una fase posterior. En lugar de rechazar el programa como mal escrito, el compilador lo pasa para la verificación en tiempo de ejecución.
El estilo se originó en Abadi et al. Y desarrollado para Haskell por Cheney y Hinze como un contenedor para representar todos los tipos dinámicos, con la clase Typeable aparece como parte del trabajo SYB de SPJ y Lammel.
Referencia
- Martín Abadi, Luca Cardelli, Benjamin Pierce y Gordon Plotkin, " Mecanografía dinámica en lenguaje estático ", ACM Transactions on Programming Languages and Systems (TOPLAS), 1991.
- James Cheney y Ralf Hinze, " Una implementación liviana de genéricos y dinámica ", Haskell ''02: Actas del taller ACM SIGPLAN 2002 sobre Haskell, 2002.
- Lammel, Ralf y Jones, Simon Peyton, " Deseche su repetición: un patrón de diseño práctico para programación genérica , TLDI ''03: Actas del taller internacional ACM SIGPLAN 2003 sobre tipos en el diseño e implementación de idiomas, 2003
- Harper, 2011, Fundamentos prácticos para lenguajes de programación.
Incluso en los libros de texto: los tipos dinámicos (con representaciones tipables) son lenguajes tipados estáticamente con un solo tipo, Harper ch 20:
20.4 Untyped Significa Uni-Typed
El cálculo λ no tipeado puede integrarse fielmente en un lenguaje tipado con tipos recursivos. Esto significa que cada término λ no tipeado tiene una representación como expresión tipada de tal forma que la ejecución de la representación de un término λ corresponde a la ejecución del término mismo. Esta incrustación no es una cuestión de escribir un intérprete para el cálculo λ en + ⇀ {+ × ⇀μ} (lo que seguramente podríamos hacer), sino más bien una representación directa de términos λ sin tipo como expresiones tipadas en un lenguaje con tipos recursivos .
La observación clave es que el cálculo λ no tipeado es realmente el cálculo λ unificado. No es la ausencia de tipos lo que le da su poder, sino que tiene un solo tipo, el tipo recursivo
D = μt.t → t.