Types dépendants

Question

Il y a quelque temps, j'ai découvert le langage de programmation Idris dont le "point de vente unique" semble être les types dépendants. Est-ce que quelqu'un peut expliquer ce que sont les types dépendants et quel genre de problème ils résolvent?

Answer 1

Eh bien, les types dépendants permettent d'exprimer des invariants de types de données qui sont vérifiés lors de la compilation. L'exemple canonique pour les types dépendants est les listes indexées par la longueur, également connues sous le nom de vecteurs. La définition des vecteurs en Idris est :

data Vec (A : Type) : Nat -> Type where
   Nil  : Vec A 0
   Cons : A -> Vec A n -> Vec A (S n)

où le type Nat correspond aux nombres naturels en notation Peano :

data Nat = Z | S Nat

Remarquez que le type Vec A est ce que l'on appelle une famille de types : pour chaque valeur n : Nat, nous avons un type Vec A n, de vecteurs de longueur n.

Avoir la longueur dans son type permet à certaines fonctions de liste d'être correctes par construction. Un exemple simple est une fonction de tête de liste sécurisée :

head : Vec a (S n) -> a
head (x :: xs) = x

Comme nous exigeons que seuls des vecteurs non vides soient passés à la fonction head - notez que l'indice S n exige des valeurs non nulles - le compilateur Idris garantit que head ne sera jamais appliqué à des listes vides.

Un autre exemple est la concaténation des vecteurs qui garantit que ses résultats ont une longueur égale à la somme de la longueur de ses paramètres :

(++) : Vec a n -> Vec a m -> Vec a (n + m)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

Remarquez que la propriété de longueur de concaténation est garantie par le type de la fonction de concaténation. Une autre application est de prouver que la fonction map traditionnelle sur un vecteur préserve sa longueur :

map : (a -> b) -> Vec a n -> Vec b n 
map f [] = []
map f (x :: xs) = f x :: map f xs

Encore une fois, la préservation de la longueur du vecteur est assurée par l'annotation de type de map. Ce sont des exemples très simples de comment les types dépendants aident à garantir des logiciels corrects par construction.

Des exemples plus convaincants de programmation typée de manière dépendante (en utilisant le langage de programmation Agda) peuvent être trouvés dans The Power of Pi. Je ne l'ai pas fait, mais je crois que tous les exemples de cet article peuvent être portés à Idris sans difficultés.