Calendrier de l'Avent - Les types dépendants

Pour ouvrir le calendrier de l’avent d’IP7 de cette année, je vous propose un article sur de la théorie des systèmes de typage (si si, je vous assure, c’est intéressant).

Tout d’abord, une rapide introduction au λ-calcul:

Le λ-calcul est un moyen de définir des programmes, qui se trouve être équivalent aux machines de Turing (attendez la suite du calendrier si vous ne connaissez pas), mais qui est beaucoup plus proche, dans son style, de la programmation fonctionelle.

Il n’y a qu’une seule construction dans le λ-calcul, c’est la fonction anonyme, notée (λx.e), ou x est le nom de l’argument et e (qui peut contenir v) le résultat. On peut appliquer la fonction f := λx.e à l’argument v en écrivant f v. (Par convention, (a b) c = a b c ≠ a (b c).) Cette expression a pour résultat e, dans lequel on a remplacé toutes les occurences de x par v.

Par exemple, on peut définir id := λv.v, qui retourne son argument, ou const := λv.λw.v, qui retourne son premier argument. Cette deuxième définition nous montre d’ailleurs comment sont encodées les fonctions à plusieurs arguments dans le λ-calcul: pour une fonction de n arguments, on fait en réalité une fonction qui prend le premier argument, et qui retourne une fonction qui prend les n - 1 arguments restant et retourne le résultat.

Avec simplement ces deux fonctions, on voit déjà le potentiel de composabilité du λ-calcul, puisqu’on peut par exemple s’en servir pour définir une fonction qui retourne son deuxième argument au lieu de son premier. Définissons-là comme suit: const₂ := const id. Vérifions qu’elle a bien le comportement attendu.

const₂ a b
= const id a b      (on remplace const₂ par sa définition)
= (λv.λw.v) id a b  (on remplace const par sa définition)
= (λw.id) a b       (on applique, en remplaçant v par id)
= (λw.λv.v) a b     (on remplace id par sa définition)
= (λv.v) b          (on applique, en remplaçant w (qui
                     n'apparait pas dans le résultat) par a)
= b                 (on applique la fonction)

Avec uniquement ces fonctions, on peut définir tous les calculs qu’on peut faire sur des ordinateurs. Un exemple que j’aime beaucoup est celui des valeurs booléennes et de leurs opérations.

vrai := λv.λw.v             (ou const !)
faux := λv.λw.w             (ou const₂ !)
si := λb.λv.λw.bvw          (ou simplement id !)
et := λb₁.λb₂.si b₁ b₂ faux
ou := λb₁.λb₂.si b₁ vrai b₂
non := λb.si b faux vrai

Essayez de calculer des exemples comme et faux vrai, ou ou faux (non faux) pour vous convaincre de la validité de ces définitions.

Et les types dans tout ça ?

Bon, on a toutes ces définitions, mais il est assez facile de faire des erreurs, en écrivant des fonctions qui ne se terminent jamais, ou même juste en donnant id en argument à une fonction qui opère sur les booléens.

Pour régler ça, définissons un système de typage très simple, qui dénote a → b une fonction qui prend un argument de type a et retourne une valeur de type b. (Notons aussi que, par convention cohérente avec celle de l’application, a→(b→c) = a→b→c ≠ (a→b)→c.) On notera ∀t. u, quand n’importe quel type t fonctionne pour u.
Observons les types que l’on peut donner à nos définitions précédentes:

id     : ∀t. t → t
const  : ∀t. t → (∀u. u → t)
const₂ : ∀t. t → (∀u. u → u)

On note, pour plus de clarté, 𝔹 := ∀t. t → t → t
vrai : 𝔹
faux : 𝔹
si   : 𝔹 → (∀t. t → t → t)   (on remarque que c'est id, avec
                              juste un type plus spécifique)
et   : 𝔹 → 𝔹 → 𝔹
ou   : 𝔹 → 𝔹 → 𝔹
non  : 𝔹 → 𝔹

Et les types dépendants ?

Eh bien, maintenant qu’on a un système de type relativement simple, on évite des erreurs, mais on est aussi assez limité (enfin, pas tant que ça, mais un peu quand même) dans les capacités de notre langage. Par exemple, on ne peut pas écrire si vrai a b si a et b sont de types différents, même si en pratique on pourrait dire que le résultat est forcément du type de a. Il serait donc pratique de pouvoir dire que le type du résultat d’une fonction dépend de la valeur de ses arguments. Par exemple, si pourrait être de type si le booléen est vrai, le résultat est du premier type, sinon il est du deuxième. Ici, on arrive aux types dépendants. À ce moment là, pour plus de simplicité, il peut être utile de dire que les types sont juste des valeurs comme les autres (nommons le type des types *).

Redéfinissons des nouveaux types (et implémentations) pour nos fonctions:

id := (λt.λv.v) : (t : *) → t → t
Notons que, puisque le premier argument est utilisé pour définir
le type du résultat, on lui donne un nom.
Notons aussi que le ∀ a disparu, remplacé par un simple argument
donné à la fonction.

const := (λt.λt'.λv.λv'.v) : (t : *) → (t' : *) → t → t' → t
const₂ := (λt.λt'.λv.λv'.v') : (t : *) → (t' : *) → t → t' → t'

Pour les booléens, comme définir le "si" comme ceci:
si := (λf.λb.λv.λw.b f v w)
    : (f : 𝔹 → *) → (b : 𝔹) → (f vrai) → (f faux) → f b
L'idée, c'est que, "si f vrai" se réduit à une fonction de type
(f vrai) → (f faux) → (f vrai), ce qui fonctionne parfaitement
pour permettre un deuxième argument de n'importe quel type,
puisqu'on retourne le premier. (C'est similaire à l'envers pour
"si f faux".)

Cette fonction f peut être définie avec des si pour faire un type
qui varie selon la valeur de b, mais peut aussi être définie comme
une constante (pour pouvoir réussir à l'utiliser sans avoir une
pile infinie de si dans le type).

Ajoutons aussi, pour compléter:
et : 𝔹 → 𝔹 → 𝔹
ou : 𝔹 → 𝔹 → 𝔹
non : 𝔹 → 𝔹
(Avec les mêmes définitions.)

Notons que je n’ai pas défini le type 𝔹 ou les valeurs de vrai et faux. C’est par-ce qu’elle ne sont pas vraiment faciles à définir sans mensonges et tours de passe-passe. Mais, en pratique, on ne les définit pas comme des types de fonction et des lambdas, mais comme des types et valeurs à part (des types algébriques, si vous avez l’habitude de la programmation fonctionelle), ce qui évite ce problème.

Et voilà, ce fut une courte introduction aux types dépendants. Attendez la suite de ce calendrier pour voir des usages de ces types de deux points de vue différents.