haskell - Promoción de tipo de datos para personas dependientes
types language-design (2)
Hay al menos dos ejemplos en el documento en sí:
"1. Introducción" dice: "por ejemplo, podríamos asegurar [en tiempo de compilación] que un supuesto árbol rojo-negro realmente tiene la propiedad roja-negra".
"2.1 Promoción de tipos de datos" trata sobre vectores indexados por longitud (es decir, vectores con errores de "índice fuera de límites" en tiempo de compilación).
También puede echar un vistazo al trabajo anterior en esta dirección, por ejemplo, la biblioteca HList para listas heterogéneas seguras de tipo y colecciones extensibles. Oleg Kiselyov tiene muchos trabajos relacionados. También puede leer trabajos sobre programación con tipos dependientes. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf tiene ejemplos introductorios para los cálculos de tipo de nivel en Agda, pero también se pueden aplicar a Haskell.
A grandes rasgos, la idea es que la head para las listas tenga un tipo más preciso. En lugar de
head :: List a -> a
es
head :: NotEmptyList a -> a
La última función de cabecera es más segura que la anterior: nunca se puede aplicar a listas vacías porque causaría errores de compilación.
Necesita cálculos a nivel de tipo para expresar tipos como NotEmptyList. Las clases de tipo con dependencias funcionales, las GAGT y las familias de tipos (indexadas) ya proporcionan formas débiles de cálculos de tipo de tipo para haskell. El trabajo que mencionas se desarrolla aún más en esta dirección.
Consulte http://www.haskell.org/haskellwiki/Non-empty_list para ver una implementación usando solo clases de tipo Haskell98.
Después de leer el ghc 7.4. notas previas a la publicación y el documento Giving Haskell a Promotion , todavía estoy confundido sobre lo que realmente hace con los tipos promocionados. Por ejemplo, el manual de GHC brinda los siguientes ejemplos sobre tipos de datos promocionados:
data Nat = Ze | Su Nat
data List a = Nil | Cons a (List a)
data Pair a b = Pair a b
data Sum a b = L a | R b
¿Qué tipo de usos tienen estos como tipos? ¿Puedes dar ejemplos (de código)?
Nat puede usar, por ejemplo, para construir vectores numéricos que solo pueden agregarse si tienen la misma longitud, verificados en tiempo de compilación .