Il arrive parfois que l'on se pose une question, qu'on ne trouve pas la réponse sur le moment, puis que cette question se rappelle à notre souvenir longtemps après.

Quand j'étais en DEA en 1998, et que j'apprenais l'encodage des types de données inductifs dans le système F (ou dans le Calcul des Constructions, même problème), je m'étais demandé si ces types pouvaient être « trop gros », c'est-à-dire contenir des termes qui ne seraient pas obtenus par application des constructeurs de ce type.

Rappelons de quoi il s'agit. On connaît bien l'encodage de Church des entiers naturels dans le λ-calcul pur : l'entier n est encodé comme une fonction qui à f associe la composée n fois de f avec elle même, soit λfλz f ( f ( … z) ). Dans le système F, on obtient ΛX λ(f: X→X) λ(x: X) f ( f ( … z) ). De même, le type des booléens peut se coder avec ΛX λ(a: X) λ(b: X) a pour « vrai » et ΛX λ(a: X) λ(b: X) b pour « faux » ; et le type Caml A of int | B of string se coderait comme le type ∀X (int→X)→(string→X)→X, avec le terme (A toto) codé par ΛX λ(a: int→X) λ(b: string→X) (a toto) et le type (B tata) codé par ΛX λ(a: int→X) λ(b: string→X) (b tata).

Selon ce même principe, le type Caml à un constructeur A of foo, trivialement isomorphe au type foo, s'encode comme ∀X (foo→X)→X, le terme (A x) s'encodant comme ΛX λ(f: foo→X) (f x). Permettez-moi maintenant une analogie (qui d'ailleurs peut sans doute se formaliser en théorie des catégorie) avec un autre domaine, l'analyse linéaire : si E est un espace vectoriel sur le corps K, et A→B désigne l'espace des applications linéaires de A dans B, alors (E→K)→K est le bidual de E, et pour tout élément x de E, λ(f: E→K) (f x) est l'élément associé par l'injection canonique de E dans son bidual. E et son bidual sont isomorphes quand E est de dimension finie, mais le bidual de E est « plus grand » que l'image de l'injection canonique de E quand E est de dimension infinie. Transposons notre doute aux types inductifs codés dans le système F : n'est-il pas à craindre que le type soit « plus gros » que l'ensemble des termes effectivement constructibles (les constructeurs étant les analogues de l'injection canonique, ce qui se comprend d'ailleurs bien dans l'interprétation catégorielle des types sommes) ?

La même question m'est revenue longtemps après, alors que je préparais un cours sur la théorie des types pour l'enseignement d'approfondissement dont je suis responsable à l'X. Ma distinguée collègue Christine Paulin a eu l'excellente idée de mettre sa remarquable thèse (de 1989 !) en ligne sur l'archive « thèses en ligne » et la réponse est au §4.3.1, p. 112 : en utilisant des types très polymorphes, il est possible de construire dans un type de la forme ∀X (N→X)→X des termes qui ne sont pas de la forme ΛX λ(f: N→X) (f n) où n est un terme clos de type N ; l'idée est que le terme n peut utiliser l'argument X dans des quantifications imprédicatives un peu compliquées.

Et là m'est arrivé une autre question, à laquelle je n'ai pas de réponse et pour laquelle je ne vois pas non plus de réponse dans la thèse de Christine Paulin...

Les constructions évoquées plus haut sont certes des termes non construits, mais je conjecture, d'une certaine façon, ils sont équivalents à des termes construits : sauf erreur de ma part, pour tout terme a du type en question, il existe un terme construit a' tel que pour tout h tel que (h a) soit d'un type construit « simple » (disons, les booléens), alors (h a)=(h a'). Autrement dit, tant qu'on ne fait pas des choses trop bizarres, les termes « en plus » ne produisent pas de comportements « inattendus ».

Il est 21 h et j'ai mal à la tête, je laisse mes lecteurs cogiter.:-)

Pour ceux que cela intéresserait, voici l'exemple de Christine Paulin, en notations pour Coq 8.3.

(Si vous voulez retrouver l'exacte définition proposée par Christine Paulin, il vous faut remplacer Type par Set et lancer Coq avec l'option -impredicative-set ; Set était naguère imprédicatif, sans doute pour permettre les codages inductifs par polymorphisme, en plus des types inductifs natifs rajoutés dans le Calcul des constructions inductives par rapport au Calcul des constructions, mais dans les versions actuelles de Coq il ne l'est plus, parce que ça posait un problème de compatibilité avec je ne sais plus quel axiome éventuellement désirable.)

Definition M (A : Type) := forall X : Type, (A->X)->X.

Definition c {A : Type} (a : A) : (M A) := fun X: Type, fun f : A->X, (f a).

Definition T := forall X : Type, X->X.

Definition t : T := fun X : Type => fun x : X => x.

Definition N := (forall D: Type, (D->T))->T.

Definition m : (M N) := fun (C : Type) (f : N -> C) => f (fun y : (forall D : Type, D->T) => y C (f (fun _ : (forall D : Type, D->T) => t))).