Polymorphisme, variables de type faibles

Code:

---

1 2 3 4 5 6

let f a b = a;;   let g = f 1;;   let h b = f 1 b;;

---

Pourquoi h est-elle polymorphe et g seulement monomorphe ?

J'ai trouvé des explications sur Internet (lien) mais j'ai beau lire et relire je ne comprends toujours pas.

Est-ce que quelqu'un pourrait donner un exemple de code qui marche avec g mais pas avec h ?

Je ne connaissais pas ça, et j'ai cherché la solution juste par intérêt, ce n'est donc pas une réponse d'expert et elle peut être incorrecte.

D'après cette FAQ, une application, même partielle, est toujours monomorphe, car elle peut avoir des effets de bords sur des éléments mutables. L'élément en question peut avoir un type indéfini lors de la définition de la fonction, mais devenir devenir défini lors de l'application. Il se peut donc que la fonction doivent changer de type après l'application.

Je ne sais pas si c'est très clair, le lien donne un bon exemple.

La réponse dans la FAQ caml officielle est ici : http://caml.inria.fr/resources/doc/f...#eta-expansion

En gros, dans la sémantique de caml, le polymorphisme est introduit seulement dans un "let" : on ne cherche à généraliser le type que lors des déclarations, le reste du temps on a un polymorphisme faible. De plus, les seules valeurs dont le type est généralisé sont les fonctions : on peut avoir des fonctions de type 'a -> 'a, mais on n'a jamais de valeurs de type 'a.

Prend par exemple la fonction id (identité), définie comme suit :

Code:

---

let id x = x

---

Cette fonction est de type 'a -> 'a.

Maintenant, on construit la valeur "id id" :

Code:

---

1 2	# id id;; - : '_a -> '_a = <fun>

---

Ce n'est pas une déclaration de fonction, caml ne généralise donc pas le type de la valeur. Il laisse un polymorphisme faible.

De même, quand on met un let :

Code:

---

1 2	# let id2 = id id;; val id2 : '_a -> '_a = <fun>

---

On a mis un let, mais ce n'est pas un let de déclaration de fonction. C'est une déclaration de valeur, qui vaut "id id". Il n'y a donc toujours pas de polymorphisme.

Code:

---

1 2	# let id2 x = (id id) x;; val id2 : 'a -> 'a = <fun>

---

Maintenant, on a explicitement précisé à OCaml que l'on construisait une valeur fonctionnelle. Alors la généralisation au niveau du let a bien lieu, et on a le polymorphisme.

Tu veux un exemple de code qui ne marche pas avec le polymorphisme faible ?

Code:

---

1 2 3 4 5 6 7 8

# let id2 x = (id id) x;; val id2 : 'a -> 'a = <fun> # (id2 1, id2 '1', id2 "1");; - : int * char * string = (1, '1', "1") # let id2 = id id;; val id2 : '_a -> '_a = <fun> # (id2 1, id2 '1', id2 "1");; This expression has type char but is here used with type int

---

Bonus :
Si tu as envie de te creuser encore un peu la tête, tu peux remarquer que la fonction

Code:

---

1 2	# let triplet id = (id 1, id '1', id "1");; This expression has type char but is here used with type int

---

ne marche pas.
C'est le sujet de la question réponse http://caml.inria.fr/resources/doc/f...phic-arguments. Bon appétit !

Citation:

---

Envoyé par http://camltest.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-fra.html#polymorphisme

La nouvelle règle pour les définition de noms:

(...)

let nom = expr1 ...

On généralise le type de expr1 quand expr1 est une fonction, un identificateur ou une constante. Sinon l'identificateur nom n'est pas polymorphe (les variables de type ne sont pas généralisées).

---

Citation:

---

Envoyé par Strab

une application, même partielle, est toujours monomorphe, car elle peut avoir des effets de bords sur des éléments mutables. L'élément en question peut avoir un type indéfini lors de la définition de la fonction, mais devenir devenir défini lors de l'application

---

Si une application partielle génère un effet de bord mais que cet effet de bord ne dépend pas d'un argument, porquoi le type de cet argument devrait-il être contraint au monomorphisme ?

Citation:

---

Envoyé par bluestorm

les seules valeurs dont le type est généralisé sont les fonctions

---

Je comprends bien que les fonctions monomorphes comme id2 ne peuvent pas être utilisées successivement avec des arguments de type différent.

Je comprends aussi que dans ton dernier exemple le type de id (argument de triplet) ne peut être inféré puisqu'il est utilisé comme une fonction mais avec des arguments de type différent.

En fait, id2 montre une conséquence du monomorphisme. Ce que je voudrais c'est une cause : pourquoi une application partielle doit-elle être monomorphe, autrement dit, si une application partielle était polymorphe, quels problèmes aurait-on ?

Pour cela je me demandais s'il était possible d'écrire un code qui fonctionnerait avec une fonction monomorphe (la fonction g de mon premier message) mais pas avec une fonction polymorphe (la fonction h de mon premier message).

La réponse est non.

En fait, le point de vue est le suivant :
Au commencement, on avait un langage fonctionnel pur.
Mais un jour, on a décidé d'ajouter des effets de bords. Alors (à cause du problème que tu connais), le typage n'était plus correct.
Il a donc fallu trouver une solution. De nombreux systèmes complexes ont été proposés (Pierre Weis en parle ici, mais il existant une solution extrêmement simple : la restriction du polymorphisme aux let de déclaration de fonctions. Pour simplifier l'implémentation du langage, les concepteurs de caml l'ont donc choisie, parce que bien que très simple elle ne pose pas de problèmes. Le cas des fonctions rejetées (que tu as découvert) est un "dommage collatéral", mais il peut être facilement résolu par êta-expansion (le fait de rajouter un argument à priori inutile).

en général, lorsque, dans un vrai code, on est confronté à ce genre de problème, c'est souvent le signe que quelque chose au niveau de la sémantique du programme n'est pas clairement défini. Bien structurer sa pensée avant de coder, c'est essentiel.

Citation:

---

Envoyé par InOCamlWeTrust

en général, lorsque, dans un vrai code, on est confronté à ce genre de problème, c'est souvent le signe que quelque chose au niveau de la sémantique du programme n'est pas clairement défini. Bien structurer sa pensée avant de coder, c'est essentiel.

---

Ce n'est pas un gros problème puisqu'on peut rendre polymorphe une application partielle en la transformant en fonction (comme l'a dit bluestorm).

En Caml c'est parfois inévitable :

Code:

---

1 2 3 4 5 6 7 8 9

# let tri_generique (f_comparaison: 'a -> 'a -> bool) (liste: 'a list) = (* ... *) liste;; val tri_generique : ('a -> 'a -> bool) -> 'a list -> 'a list = <fun>   # let tri_croissant = tri_generique (<);; val tri_croissant : '_a list -> '_a list = <fun>   # let tri_croissant liste = tri_generique (<) liste;; val tri_croissant : 'a list -> 'a list = <fun>

---

Dans cet exemple, la première fonction tri_croissant est monomorphe (le type est inconnu mais sera déterminé définitivement à la première utilisation) alors que la deuxième est polymorphe.

Voici un exemple qui explique le pourquoi de cette restriction :

Code:

---

1 2 3 4 5 6 7 8 9 10

let f _ = let c = ref [] in fun b -> c := b :: (!c);;   let g = f 2;; '_a -> unit   let h x = f 2 x;; 'a -> unit

---

Si la fonction g était polymorphe, on pourrait l'appliquer successivement à variables de types différents et donc la variable c dans f contiendrait une liste hétérogène (en types). En effet, la variable c est instanciée après que le premier argument de la fonction f ait été fourni, et c'est le cas de la fonction g (f 2 est exécuté au moment de la définition de g tandis que dans la fonction h, f 2 x est exécuté à chaque appel de h).

Voilà.

Je suis d'accord avec boromir73, le cas le plus courant c'est avec les fonctions (<) , (>) , compare et autres, et dans ce cas c'est une η-expansion qui s'impose.

Exemple:

Code:

---

1 2 3 4 5 6 7 8 9 10 11

let map_merge cmp f a b = let rec loop a b u = match a,b with | [],_ -> List.rev_append u b | _,[] -> List.rev_append u a | ha::ta,hb::tb -> let c = cmp ha hb in if c < 0 then loop ta b (ha::u) else if c > 0 then loop a tb (hb::u) else loop ta tb (f ha hb::u) in loop a b [];;

---

Code:

---

1 2	# let merge_list = map_merge compare (fun a b -> b);; val merge_list : '_a list -> '_a list -> '_a list = <fun>

---

Après une η-expansion:

Code:

---

1 2	# let merge_list l = map_merge compare (fun a b -> b) l;; val merge_list : 'a list -> 'a list -> 'a list = <fun>

---

Je vois trois possibilités:

• vous attendiez un type polymorphe: appliquez une η-expansion
• vous attendiez un type monomorphe: ajoutez une annotation de type
• vous n'attendiez rien du tout: c'est le cas traité par InOCamlWeTrust, vous ne savez pas ce que vous faites, sinon vous attendriez un type, vous devriez toujours attendre un type