Re: théorie des ensembles pas naives

Devrais-je clarifier dans la LEP que quand je dis "ils n'ont pas de type" je parle de "type" au sens IT du terme?

Je ne vois toujours pas en quoi ils n'ont pas de type au sens IT du terme. Un type c'est un ensemble de valeurs (comme N, Q ou R), et la notion d'ensemble au sens "naïf", telle qu'utilisée en mathématiques, est bien plus proche de celle de type que de celle d'ensemble au sens de ZFC (personnellement, je préfère de loin les théories de types comme fondements des mathématiques à ZFC).

Après, ton système de classe revient à appliquer le principe de la définition par compréhension, ce qui génère des sous-types de ton type d'entrée. En OCaml, on pourrait formuler le principe général ainsi :

module Comprehension (M : sig type t val prop : t -> bool end) : sig
 type t = private M.t
 val make : M.t -> t
end = struct
 type t = M.t
 let make x = if M.prop x then x else failwith "make"
end

Le schéma de compréhension prend en entrée un type t ainsi qu'un propriété sur ce type, puis renvoie en sortie le sous-type (ou sous-ensemble) des éléments de t qui satisfont la propriété. Exemple avec le type even :

module Even = Comprehension (struct
 type t = int
 let prop x = x mod 2 = 0
end)
let deux = Even.make 2;;
val deux : Even.t = 2
(* ici `deux` est considéré comme de type `Event.t` et non comme `int` *)
deux + 3;;
Line 1, characters 0-4:
Error: This expression has type Even.t but an expression was expected of type
 int
(* mais on peut aussi le caster vers un `int` *)
(deux :> int) + 3;;
- : int = 5

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