Re: Un peu déçu par Rust

Certes, mais même lorsque l'on fait du typage statique et que l'on utilise un algorithme d'unification, il est possible de renvoyer des messages plus compréhensibles. Le papier auquel tu renvoies donne des pistes, mais le message de Guillaume Denry sur elm est encore plus parlant. Elm a un système de type à la Haskell et son message d'erreur est on ne peut plus compréhensif et informatif.

Comme ces derniers temps je joue un peu avec Coq, qui doit faire face à des problématiques d'unification à coté desquelles celles de Rust sont un jeu d'enfant, je vais donner des exemples dans ce langage.

Pour commencer, il semblerait naturel de n'utiliser une notation infixe x + y que dans une structure de monoïde. Alors je vais le faire façon type classes à la Haskell :

Class monoid {A : Type} (op : A -> A -> A) (e : A) := {
 _ : forall x y z, op x (op y z) = op (op x y) z ;
 _ : forall x, op e x = x ;
 _ : forall x, op x e = x }.
Generalizable Variables A op e.
Definition monoid_op `{M : monoid A op e} x y := op x y.
Infix "+'" := monoid_op (at level 50).

Là on fait un type checking sur la fonction monoid_op :

Check monoid_op.
(* ==>
monoid_op
 : ?A -> ?A -> ?A
where
?A : [ |- Type] 
?op : [ |- ?A -> ?A -> ?A] 
?e : [ |- ?A] 
?M : [ |- monoid ?op ?e] *)

Elle prend deux valeurs d'un certain type ?A et renvoie une valeur de ce type, et cela dans un contexte où ce type est connu avec un monoïde sur les valeurs de ce type (le ? signifie que le terme est indéterminé, la variable est existentielle : il existe une valeur A telle que ...). Si on lui demande de typer l'expression 1 +' "3a", on obtient :

Check 1 +' "3a".
(* ==>
Error:
The term ""3a"" has type "string" while it is expected to have type "nat". *)

Mais le plus amusant est qu'il peut typer le terme "1" +' "3a" avant même de savoir le calculer :

Check "1" +' "3a".
(* ==>
"1" +' "3a"
 : string
where
?op : [ |- string -> string -> string] 
?e : [ |- string] 
?M : [ |- monoid ?op ?e] *)
Eval compute in "1" +' "3a".
(* ==>
 = ?op "1" "3a"
 : string *)

Maintenant pour lui permettre de calculer, on lui fournit une instance de la classe :

(* on prouve que le type string muni de l'opération de concaténation
 est un monoïde dont l'élément neutre est la chaîne vide. *)
Instance Str_append : monoid append "".
Proof.
split.
- induction x; [auto | intros; simpl; rewrite IHx; reflexivity].
- reflexivity.
- induction x; [auto | simpl; rewrite IHx; reflexivity].
Qed.
(* maintenant on vérifie le type et on évalue : *)
Check "1" +' "3a".
(* ==>
"1" +' "3a"
 : string *)
Eval compute in "1" +' "3a".
(* ==>
 = "13a"
 : string *)

Pour le cas plus général où les deux opérandes ne sont pas du même type (et l'on se demande bien alors pourquoi utiliser la notation additive ?), et revenir à la situation de python, je vais l'illustrer ainsi.

Class bin_op (A B C : Type) := op : A -> B -> C.
Infix "+'" := op (at level 50).
Check 1 +' "3a".
(* ==>
1 +' "3a"
 : ?C
where
?C : [ |- Type] 
?bin_op : [ |- bin_op nat string ?C] *)

Là on est dans la situation de python : comme il fait du typage dynamique, lors de l'appel au calcul de l'expression il vérifie si l'environnement permet de bien typer le terme (s'il peut instancier ces variables existentielles). Comme ce langage permet de modifier dynamiquement l'environnement, il est impossible de refuser statiquement ce code. Il pourrait, par exemple, être défini dans une bibliothèque où le code ne peut être évalué, puis importer dans un code qui rend l'évaluation possible. Comme dans le dialogue suivant avec la REPL Coq :

Eval compute in 1 +' "3a".
(* ==>
 = ?bin_op 1 "3a"
 : ?C *)
(* ici l'évaluation totale génère une erreur : le typage étant statique,
 il exige d'être dans un environnement où les variables existentielles
 sont instanciées. *)
Eval vm_compute in 1 +' "3a".
(* ==>
Error: vm_compute does not support existential variables. *)
Instance nat_add : bin_op nat nat nat := {op := plus}.
Instance str_app : bin_op string string string := {op := append }.
Instance nat_str : bin_op nat string string := {
 op n s:=
 match get n s with 
 | None => ""
 | Some c => String c ""
 end }.
Eval vm_compute in 1 +' 3. (* ==> 4 : nat *)
Eval vm_compute in "1" +' "3a". (* ==> "13a" : string *)
Eval vm_compute in 1 +' "3a". (* ==> "a" : string, à la manière du C *)

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