Re: Un peu déçu par Rust

Au niveau du système de module, des annotations de types sont nécessaires pour les arguments des foncteurs:

module F(X:sig type t end (* ← ceci est une annotation de type *)) = 
struct include X end (* mais le type (i.e. la signature) de retour est inferré *)

Les modules récursifs eux ont besoin d'être totalement annoté, par exemple:

module rec M : (* ↓ annotation du type de M *)
sig
 type t = A of S.t 
 val compare: t -> t -> int
end = struct
 let compare = compare
 type t = A of S.t
end
and S : (Set.S with type elt = M.t) (* ← annotation du type de S *) 
= Set.Make(M);;

Ce besoin d'annotation pour les modules peut se propager dans les fonctions à cause
des modules locaux (ou de première classe).

let dedup (type a (* ←soit un type a abstrait*) ) l = 
 (* ici on a besoin d'introduire un type a pour le module S définit ci-dessous *)
 let module S = Set.Make(struct type t = a let compare = compare end) in
 S.elements @@ S.of_list l

Un autre cas classique d'annotation explicite apparaît pour la récursion polymorphique
sur les types récursifs non homogènes:

type 'a arbre_complet = Feuille of 'a | Noeud of ('a * 'a) arbre_complet
let rec hauteur: 'a.(*← ∀a *) 'a arbre_complet -> int = function
 | Feuille _ -> 0
 | Noeud a ->
 (* dans cette branche, hauteur est appliqué à ('a * 'a) arbre_complet *) 
 1 + hauteur a

Dans ce cas, l'annotation 'a.'a arbre_complet -> int qui équivaut à forall 'a....
est nécessaire car le type du paramètre 'a à l'intérieur de la définition de hauteur et à l'extérieur diffère.

Pour le polymorphisme de second ordre, OCaml ne supporte pas directement les annotations forall à l'intérieur des arguments de fonctions, il faut donc passer soit par des types enregistrements(records):

type id = { f:'a. 'a -> 'a }

ce qui est plus contraignant qu'une annotation directe, soit par le système objet

let pair (id: <f:'a.'a -> 'a>) = id#f 1, id#f []

Sans cette annotation le typeur va essayer d'unifier le type de 1 et [] et renvoyer une erreur.

Les GADTs de leur côté sont toujours lourds en annotations en Haskell ou OCaml

 type 'a monoid =
 | R: float monoid
 | N: int monoid 
 | Pair: 'a monoid * 'b monoid -> ('a * 'b) monoid
 let rec zero: type a. (*← ∀a, a abstrait *) a monoid -> a = function
 | R -> 0. (* ← dans cette branche, a = float *)
 | N -> 0 (* ← a = int *)
 | Pair (a,b) -> zero a, zero b (* a = b * c *)

Enfin, une particularité d'OCaml du aux effets de bords, ce sont les types faiblement polymorphiques, qui ne peuvent pas être exporté par une unité de compilation, ce qui peut nécessiter d'ajouter des annotations de type pour les éliminer. Par exemple, un fichier a.ml

 let x: int list ref = ref []

ne compile pas sans son annotation de type.