Comme déjà dit par Thomas Douillard, c'est le calcul des constructions (une théorie des types) qui est à la base de Coq. Pour OCaml, le système de types qui s'en rapproche le plus c'est le système F de Jean-Yves Girard. Par contre, utiliser les modules OCaml pour éviter les paradoxes n'est pas un bon choix. Leo White a implémentéle paradoxe de Girard dans le système de modules de OCaml.
D'une manière générale, il me semble que si la logique sous-jacente d'un système de types est non contradictoire, alors le système de calcul associé n'est pas turing complet (ce qui est, par exemple, le cas de Coq); ce qui n'est pas une propriété désirée pour un langage généraliste.
Après, il y a un point que je ne comprends pas trop dans la LEP de David Delassus, lorsqu'il dit que les objets mathématiques n'ont pas de types. Pour moi les mots types et concepts mathématiques sont synonymes, donc si, les objets mathématiques ont tous un type (type qui, certes, n'est pas unique : les entiers sont des rationnels, qui sont eux-mêmes des réels, qui sont des complexes...)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: théorie des ensembles pas naives
Posté par kantien . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 3.
Comme déjà dit par Thomas Douillard, c'est le calcul des constructions (une théorie des types) qui est à la base de Coq. Pour OCaml, le système de types qui s'en rapproche le plus c'est le système F de Jean-Yves Girard. Par contre, utiliser les modules OCaml pour éviter les paradoxes n'est pas un bon choix. Leo White a implémenté le paradoxe de Girard dans le système de modules de OCaml.
D'une manière générale, il me semble que si la logique sous-jacente d'un système de types est non contradictoire, alors le système de calcul associé n'est pas turing complet (ce qui est, par exemple, le cas de Coq); ce qui n'est pas une propriété désirée pour un langage généraliste.
Après, il y a un point que je ne comprends pas trop dans la LEP de David Delassus, lorsqu'il dit que les objets mathématiques n'ont pas de types. Pour moi les mots types et concepts mathématiques sont synonymes, donc si, les objets mathématiques ont tous un type (type qui, certes, n'est pas unique : les entiers sont des rationnels, qui sont eux-mêmes des réels, qui sont des complexes...)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.