Type produit et compagnie

Temps de lecture : 4 minutes 25/06/2020 #maths #info #théorie-des-types

Un truc qui peut sembler étrange quand on fait de la programmation, et surtout de la programmation fonctionnelle, c'est les noms « type produit » et « types sommes » (dans les autres styles de programmation, le système de type est assez différent pour que cette distinction n'existe pas en général). J'ai pas l'impression qu'en Haskell on en parle tant que ça, mais en OCaml c'est le cas, donc je vais utiliser des exemples de code en OCaml dans la suite principalement je pense.

Logiquement, on aurait envie de dire que ça :

type truc = int * string

C'est un type « somme » : on a un int plus (+) un string. Mais pourtant, on utilise un signe * qui sert normalement pour la multiplication, et on appelle ça un type produit. Pourquoi ?

Types et ensembles

Une première réponse pourrait être de dire qu'un type, c'est l'équivalent informatique d'un ensemble en maths. Si on dit

$$x \in \mathbb{N}$$

et x : int, c'est un peu la même chose. On dit quel type (haha) de valeurs x peut prendre.

Et un truc qu'on peut faire avec les ensembles en maths, c'est un produit cartésien. La définition formelle fait peur :

$$ \forall A, \forall B, \exists P, \forall z (z \in P \iff \exists x \exists y (x \in A \land y \in B \land z = (x, y))) $$

mais l'idée est très simple : on forme un nouvel ensemble qui contient tous les couples qu'on peut créer avec les deux ensembles dont on part.

Ça ressemble beaucoup à un type produit donc ! On pourrait prendre :

$$ X = \lbrace 1 ; 2 \rbrace ; Y = \lbrace 3 ; 4 \rbrace ; P = X \times Y $$

et le code suivant :

type x = Un | Deux
type y = Trois | Quatre
type p = x * y

et les valeurs possibles d'un élément de P seraient équivalentes aux valeurs que peut prendre une variable de type p.

Mais il y a une explication que je trouve beaucoup plus sympa, même si beaucoup plus complexe.

Booléens et Curry-Howard

On va prendre l'ensemble suivant.

$$ B = \lbrace 0 ; 1 \rbrace $$

Et on définit dessus une addition et une multiplication.

L'addition donne 1 si on additionne au moins un 1, et 0 si on additionne deux 0. Par exemple, 0 + 1 = 1, 0 + 0 = 0 et 1 + 1 = 1. Et la multiplication donne 0, sauf si on multiplie 1 par 1.

Si on regarde bien, on peut faire de la logique avec ce petit ensemble : si on dit que le 0 correspond à une proposition fausse, et le 1 à une proposition vraie, l'addition et la multiplication peuvent servir respectivement de ou et de et. Ainsi, « vrai ou faux » peut s'écrire : 0 + 1, ce qui vaut 1, soit « vrai ».

Et c'est un peu ce qui se passe dans un ordinateur quand on fait des opérations sur des booléens au final : ils sont représentés avec des 0 et des 1, et on peut donc utiliser ces opérations qui semblent être faites pour des nombres sur des valeurs « vrai » ou « faux ».

Et là où tout se rejoint, c'est avec la correspondance de Curry-Howard. C'est un truc qui dit, en gros, qu'un type en informatique et qu'une proposition en logique c'est la même chose.1 Pour chaque proposition, on peut écrire un type qui correspond, et si on arrive à créer une valeur de ce type, alors on a une preuve de la proposition. Sinon, c'est soit que la proposition est fausse, soit qu'elle est indémontrable.

Et en particulier, si on a deux propositions A et B, la proposition A et B correspondra à un type produit.2

(* 'a et 'b sont deux types quelconques *)
type ('a, 'b) a_et_b = 'a * 'b

Du coup le « et » booléen et le « et » de la correspondance de Curry-Howard peuvent être vus comme un produit.

Et je trouve ça grave… cool (je sais pas si c'est le bon mot, mais on va dire que oui) que tout semble cohérent quelque soit le point de vue qu'on prenne.

J'aime les maths.

1

Quand j'ai découvert ça mon cerveau a explosé, je trouve ça fou.

2

Les types sommes eux, c'est des « ou ».