Re: Reason

En dehors du fait de recourir à un système de types dépendants, je ne vois pas comment on peut mélanger types et valeurs ensembles. On peut mélanger des types avec des types en C++ avec les templates, en Java avec les generics, en Haskell ou OCaml avec les types paramétrés. Mais mélanger des types et des valeurs comme paramètres de fonctions, c'est ce que font seuls les types dépendants. Je ne sais si c'est très gênant, mais cela ne permet effectivement pas d'exprimer certaines contraintes logiques dans le système.

le type des entiers non nuls se définie ainsi en Coq :

Definition non_nul := {n : nat | n <> 0}.

C'est ce que je connaissais des types paramétriques. Le problème est que d’accepter n'importe quoi comme équation booléenne rend la vérification très compliquée.

Ce n'est pas une équation booléenne. Le terme n <> 0 (ou not (n = 0)) n'est pas un booléen mais une proposition.

Check not (1 = 0).
(* la réponse de coqide est :
 1 <> 0
 : Prop
*)

Les propositions sont susceptibles d'être prouvées (ou non), mais ce ne sont pas des booléens qui valent true ou false.

Check true.
(* réponse de coqide
 true
 : bool
*)

Ainsi un habitant du type non_nul est la donné d'une valeur n de type nat ainsi que d'une preuve qu'elle est non nulle. Voir le paragraphe Propositions and booleans de Software Foundations. Se représenter la logique comme un calcul sur les booléens est une vision réductrice de cette science.

Lors de la traduction de Coq en OCaml, tout les habitants du type Prop sont effacés : ils servent à exprimer la spécification du code mais disparaissent à la compilation, de la même façon que les informations de typage disparaissent à la compilation en OCaml.

Si on ne veut pas aller jusqu'à utiliser Coq pour réaliser ce genre de chose, il est toujours possible de faire quelque chose d'approchant en OCaml avec les GADT. Mais cela relève déjà d'un usage avancé du système de types. Voir le chapitre 8.1.2 Depth indexing imperfect trees p.13. Les GADT servent ici à encoder des preuves qui seront construites dynamiquement (à l'exécution) et qui paramétreront le type des arbres.

Enfin tu devrais jeter un œil au système des modules et des foncteurs du langage. Lorsque tu parles d'une technologie de bus particulière A429 ainsi qu'une instance de cette technologie, cela peut peut être s'exprimer avec des signatures (définition générale de la technologie) et des modules (une implémentation particulière ce celle-ci).

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