Re: théorie des ensembles pas naives

Peu importe, on est censé pouvoir additionner les deux.

Mais, on le peut ! Il est tout à fait possible d'ajouter des nombres pairs et des nombres impairs, en les considérant en tant que int. C'est juste qu'il y une annotation explicite de typage pour dire cela au type checker; mais la valeur deux de mon exemple précédent est bien à la fois de type Event.t et de type int.

Ce que tu fais, c'est du sous-typage : c'est le cœur de la logique des classes d'Aristote. J'en avais parlé lors d'une dépêche sur OCaml pour expliquer la distinction entre héritage et sous-typage, et la différence fondamentale entre le système objets d'OCaml et celui de Java (par exemple).

Il n'y pas que les objets mathématiques qui ont plusieurs types, tous les êtres sont ainsi. Par exemple, Socrate est un homme mais c'est aussi un animal, un philosophe grec... Si tu sais que tous les animaux sont mortels et que Socrate est un homme, pour pouvoir appliquer le premier principe à Socrate (et conclure qu'il est mortel), il faut justifier du fait que c'est un animal, ce que tu peux faire si tu sais que les hommes sont des animaux.

• Tous les animaux sont mortels
• Tous les hommes sont des animaux
• or Socrate est un homme
• donc Socrate est un animal
• donc Socrate est mortel

La hiérarchie entre les concepts mortel, animal, homme : c'est ça le sous-typage. En OCaml, lorsque j'écris ceci :

type t = private M.t

j'affirme au type-checker que tous les t sont des M.t ou, de manière équivalente, que t est un sous-type de M.t. Ainsi par application du principe de définition par compréhension, on obtient que tous les Event.t sont des int. Après quand je veux appliquer la fonction +, dont le type est int -> int -> int, avec parmi les paramètres la valeur deux : Event.t, il se passe deux choses. Dans un premier temps, je ne dis pas au type checker que je veux oublier la parité de deux, alors il se plaint, les deux types int et Event.t étant distincts (tous les entiers ne sont pas pairs). Par contre si je lui dis que je veux oublier sa parité et le voir comme un int en écrivant deux :> int, il valide le tout car il sait que les Event.t sont des int et que donc deux est bien aussi un int.

Cela étant, je tiens à signaler que tout ceci est réalisé statiquement (le code non annoté refuserai de compiler), ce qui n'est pas le cas de LetLang d'après tes specs. La différence étant que les cast doivent être explicites en OCaml.

Après, il y a un point non abordé dans ta spec : quid des listes de even ? Sont-elles des listes de number ? Si c'est le cas, il te faudra aborder la notion de variance (invariance, covariance et contravariance) des types paramétriques. Exemple en OCaml :

(* une fonction qui somme une liste de `int` *)
let sum l = List.fold_left (+) 0 l;;
val sum : int list -> int = <fun>
(* la somme des 3 premiers `int` *)
 sum [1; 2; 3];;
- : int = 6
(* elle somme aussi les listes de `Event.t`, le type list étant covariant *)
sum ([deux; deux] :> int list);;
- : int = 4

Je ne suis pas sûr que tu te sois posé la question, car d'après ta spec sur les fonctions, on peut lire :

NB: The class func[arguments -> return] contains every function with the same signature.

Pourtant les types des fonctions -> est contravariant sur son entrée (arguments) et covariant sur sa sortie (return). Ainsi la classe func[number -> number] devrait aussi contenir les fonctions avec cette signature func[number -> int] (si on retourne un int, on retourne aussi, a fortiori, un number).

let foo (f : int -> int) x = f x;;
val foo : (int -> int) -> int -> int = <fun>
(* je peux appliquer `foo` a une fonction de type `int -> Event.t` *)
let bar (f : int -> Even.t) = foo (f :> int -> int);;
val bar : (int -> Even.t) -> int -> int = <fun>

Bonjour la condescendance. De une je n'ai jamais prétendu être un expert, de deux je présente un système de type inspiré de la théorie des ensembles, et non inspiré d'une quelconque théorie des types (car il y en a plusieurs).

Ce n'était pas de la condescendance, juste un peu d'agacement de ma part au ton perçu (peut-être à tort) de ton message. Et j'avais lu ta spec : tu t'inspires de l'approche de Russel et Whitehead dans leur principia mathamtica. Je voulais juste signaler que la proposition selon laquelle les objets mathématiques n'avaient pas de type été fausse (au sens IT ou non du terme, sens qui reste somme toute assez flou). Tu prends le partie de la compréhension sur celui de l'extension en ce qui concerne un concept. Un concept pouvant être envisagé de deux points de vue : celui de la compréhension (les conditions sous lesquelles un objet tombe sous un concept, ce qui en constitue sa définition) ou celui de son extension (la totalité des choses qui tombent sous ce concept, ce qui en fait une collection, un ensemble de choses). Tu prends le partie de la compréhension est en fait un fonction qui retourne un booléen, fonction qui ne sera appliquée qu'à l'exécution.

Cela étant, il y a un point qui m'intrigue dans ta spec. Tu prétends avoir rejeté l'idée d'un classe object qui contiendrait toutes les valeurs du langage, parce que cela irait à l'encontre de la hiérarchie des set. Mais qu'en est-il de cette classe que je semble pouvoir définir ?

class object (v : !even | even)

De ce que je comprends, sa fonction de compréhension vaut true pour toutes valeurs du langage, et donc l'extension de cette classe contiendrait bien toutes les valeurs.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.