Re: théorie des ensembles pas naives

AAAAAAAAAAAAAAH.... merci. Il va falloir que j'ajoute à ma TODO d'interdire ce genre de définition (il me semble que des outils comme coq pourrait m'aider à implémenter cette fonctionnalité).

Je ne suis pas certain qu'il soit nécessaire d'interdire ce genre de définition. Dans ton langage, comme tu peux raffiner un type à l'exécution, le type object c'est juste le interface {} du Go. Tu perds toute information de typage, mais ce n'est pas en soit dangereux, juste peut utile du point de vue typage. Et si on ne peut pas raffiner le type, c'est juste un singleton (même s'il semble contenir plus de valeurs en apparence) : voir cette discussion sur le forum OCaml.

Après, d'une manière générale, comme te l'a fait remarquer Octachron, tu ne précises rien sur la hiérarchie des univers : si even et !even était dans le même univers, le type even | !even ne contiendrait pas toutes les valeurs.

Enfin, avoir une contradiction dans le système de types (vu comme une logique) n'est pas si grave si tu ne cherches pas à implémenter un assistant de preuves. Dès que tu as de la récursion générale, c'est inévitable.

let rec f x = f x;;
val f : 'a -> 'b = <fun>
(* l'équivalent de ton type `never` *)
type never = |
(* et pourtant il n'est pas vide, un calcul qui ne termine pas peut recevoir ce type *)
let _ : never = f ()
(* ou encore avec une exception *)
let _ : never = failwith "faux"

Plus d'infos sur cette présentation de la correspondance de Curry-Howard.

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