Promotion de type de données pour les personnes à charge

Question

Après avoir lu le ghc 7.4. Les notes de pré-version et le papier de promotion de Giving Haskell , je ne comprends toujours pas ce que vous faites réellement avec les types promus. Par exemple, le manuel GHC donne les exemples suivants sur les types de données promus:

 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
 

Quels types d'utilisations ont-ils comme types? Pouvez-vous donner des exemples (de code)?

Answer 1

Il y a au moins deux exemples dans le document lui-même:

"1. Introduction", dit: "par exemple, nous pourrions être en mesure d'assurer [au moment de la compilation] qu'une prétendue rouge-noir arbre a vraiment le rouge-noir à la propriété".

"2.1 la Promotion de types de données" explique longueur indexés sur les vecteurs (qui est, avec des vecteurs au moment de la compilation "index out of bounds" erreurs).

Vous pouvez également jeter un oeil à des travaux antérieurs dans ce sens, par exemple, HList bibliothèque de type-safe hétérogène listes et extensible collections. Oleg Kiselyov a beaucoup de travaux connexes. Vous pouvez également lire les travaux sur la programmation avec des types dépendants. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf a introduction exemples de type de niveau de calculs dans Agda, mais ceux-ci peuvent être appliquées à Haskell ainsi.

En gros, l'idée est que l' head pour les listes de manière plus précise le type. Au lieu de

head :: List a -> a

il est

head :: NotEmptyList a -> a

Le dernier chef de la fonction est plus typesafe que l'ancienne: il ne peut être appliquée à vide listes car elle provoquerait des erreurs du compilateur.

Vous avez besoin au niveau du type de calculs pour exprimer les types comme NotEmptyList. Les classes de Type avec dépendances fonctionnelles, GAGTs et (indexée) type de familles fournissent déjà des formes faibles de niveau du type de calculs pour haskell. Le travail que vous avez mentionné juste des précisions plus loin dans cette direction.

Voir http://www.haskell.org/haskellwiki/Non-empty_list pour une mise en œuvre à l'aide de seulement Haskell98 type de classes.