Discussion :

[SpiceGuid]

À moins d'une inattention de ma part, le manuel officiel, au chapitre 6.4, passe totalement sous silence cette construction de type :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
poly-typexpr ::= typexpr
             |  { 'ident }+ . typexpr

En jouant un peu:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
# type func = {f:'a.('a -> 'a)};;
type func = { f : 'a. 'a -> 'a; }
# {f=fun x -> x};;
- : func = {f = <fun>}

Il semble que cette notation corresponde à la notion de quantification universelle de type.

Evidemment, dans mon exemple ci-dessus il est impossible que f soit autre chose que l'identité.

Dans ces conditions, on peut se demander:

• où trouver de la documentation sur la quantification universelle de type en Ocaml ?
• cette fonctionnalité a-t-elle une possible utilité en dehors de la POO à la sauce OCaml ?
• si oui alors quel genre de problème cette construction est-elle sensée résoudre ?

[gasche]

Each method may have an explicit polymorphic type: { ' ident }+ . typexpr. Explicit polymorphic variables have a local scope, and an explicit polymorphic type can only be unified to an equivalent one, with polymorphic variables at the same positions.

Cette fonctionnalité est disponible dans le type des enregistrements et des objets. Il me semble que cela vient du fait qu'elle a été introduite pendant la construction de la partie "objet" de OCaml (son utilité majeure c'est de rendre typable des concepts POO louches).
Elle est d'ailleurs évoquée dans la partie du manuel traitant des objets (http://caml.inria.fr/pub/docs/manual...manual005.html, chercher "'a.").

cette fonctionnalité a-t-elle une possible utilité en dehors de la POO à la sauce OCaml ?

Ça dépend de ce que tu appelles "POO". Parfois (mais c'est assez rare) on a l'impression d'avoir besoin, les Haskelliens l'utilisent par exemple. Après, on peut souvent réduire ces cas à de "l'approximation de POO" (il me semble que les implémenteurs de la POO en OCaml considèrent ce truc, avec le sous-typage, comme étant l'essence de la POO).

si oui alors quel genre de problème cette construction est-elle sensée résoudre ?

Exemple typique :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
let test (f : 'a -> unit) = (f (), f "foo");;
This expression has type string but is here used with type unit

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# let test (f : < poly : 'a. 'a -> unit >) = (f#poly (), f#poly "foo");;
val test : < poly : 'a. 'a -> unit > -> unit * unit = <fun>

[Jedai]

Ça dépend de ce que tu appelles "POO". Parfois (mais c'est assez rare) on a l'impression d'avoir besoin, les Haskelliens l'utilisent par exemple. Après, on peut souvent réduire ces cas à de "l'approximation de POO".

Pas toujours néanmoins. Par exemple la monade ST en Haskell utilise les types polymorphiques de rang 2 pour garantir statiquement qu'elle restera pure vue de l'extérieur, bien qu'elle autorise des effets de bord en interne.

--
Jedaï

[SpiceGuid]

Je comprends mieux, il s'agirait donc de fabriquer du polymorphisme là où la règle du let-bound polymorphism interdit de l'inférer. Et ça concerne tout composant d'un enregistrement qui a une valeur fonctionnelle qu'on voudrait polymorphe, c'est forcément POO, ou au moins c'est dans le style POO :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
# type func = {f:'a.('a -> unit)};;
type func = { f : 'a. 'a -> unit; }
# let test m = (m.f (), m.f "foo");;
val test : func -> unit * unit = <fun>

[alex_pi]

Enfin tout ça, c'est surtout dans le style Système F! D'ailleurs, peut être qu'un jour, MLF (de Didier Rémy) sera votre ami pour ce genre de chose :-)

[SpiceGuid]

Le polymorphisme de second ordre (ou de rang 2) c'est un synonyme pour la quantification universelle de type ?

[gasche]

Pas vraiment. Il y a déjà quantification universelle dans les types paramétrés. Ce qu'apporte le polymorphisme de second-ordre, d'où son nom, c'est de pouvoir manipuler comme des types normaux les types polymorphes.

Cela se voit bien dans les deux définitions suivantes :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 type ('a, 'b) apply = { app : ('a -> 'b) -> 'a }
type 'a polyapp = { papp : 'b . ('a -> 'b) -> 'b }

Dans le premier cas, les deux paramètres sont "en dehors" du record. Cela peut se lire en quelque sorte (disclaimer : je n'ai aucun background théorique sur la question donc je fais uniquement part de mon expérience, non rigoureuse) "quel que soit le type 'a, quel que soit le type 'b, je peux construire une valeur { app : ('a -> 'b) -> 'a }".

Dans le deuxième cas, le deuxième quantificateur est placé "à l'intérieur" du record : "quel que soit le type 'a, je peux construire une valeur qui, pour tout type 'b est de type ('a -> 'b) -> 'b ". Cela veut dire que le type de 'b n'est pas déterminé par le choix de la valeur.

Cela se voit vite à l'utilisation :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
# let to_apply a = { app = fun f -> f a };;
val to_apply : 'a -> ('a, 'b) apply = <fun>
# let test = to_apply 1;;
val test : (int, '_a) apply = {app = <fun>}
# test.app float;;
- : float = 1.
# test.app string_of_int;;
This expression has type int -> string but is here used with type
  int -> float

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
# let to_polyapp a = { papp = fun f -> f a };;
val to_polyapp : 'a -> 'a polyapp = <fun>
# let test2 = to_polyapp 1;;
val test2 : int polyapp = {papp = <fun>}
# test2.papp string_of_int;;
- : string = "1"
# test2.papp float;;
- : float = 1.

Le deuxième cas est plus polymorphique.

On dit "de second ordre" parce que dans le deuxième cas le quantificateur est "à l'intérieur" du type et pas uniquement en dehors. On a en fait construit un schéma de typage à partir d'une valeur elle-même polymorphe (le type de papp). Par analogie, quand une fonction va d'une valeur du langage à une valeur du langage (où "valeur" veut dire int, float, etc., pas une fonction), on dit qu'elle est de "premier ordre", et si le langage autorise une déclaration de fonctions qui passe en argument ou renvoye des fonctions de premier ordre, alors cette fonction est "de second ordre".

Les langages fonctionnels ont des "higher order functions" (d'ordre supérieur ?), c'est à dire que l'on peut passer des fonctions d'ordre quelconque. L'analogie au niveau du typage serait le fait de pouvoir construire des fonctions polymorphes d'ordre quelconque (en gros, avec une imbrication de termes et de quantificateurs arbitrairement profonde). Il me semble que c'est impossible parce qu'alors le système de typage acquiert toute la puissance logique du système des prédicats, et la question de la décidabilité du typage revient plus ou moins, si je ne m'imagine rien, à du "peut on prouver toute proposition de la logique des prédicats ?", ce qui n'est pas vraiment de la tarte.

[NokyDaOne]

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
 
# let to_apply a = { app = fun f -> f a };;
val to_apply : 'a -> ('a, 'b) apply = <fun>
# let test = to_apply 1;;
val test : (int, '_a) apply = {app = <fun>}
# test.app float;;
- : float = 1.
# test.app string_of_int;;
This expression has type int -> string but is here used with type
  int -> float

ça c'est le vieux bug caml. Il ne sait pas que f x = g x est la même chose que f = g (si l'on est sur que ce sont des fonctions)
j'ai le même pb en faisant :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
 
#let to_apply x f = f x;;
val to_apply : 'a -> ('a -> 'b) -> 'b = <fun>
#let un = to_apply 1;;
val un : (int -> '_a) -> '_a = <fun>

mais si l'on fait

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
 
#let to_apply x f = f x;;
val to_apply : 'a -> ('a -> 'b) -> 'b = <fun>
#let un f = to_apply 1 f;;
val un : (int -> 'a) -> 'a = <fun>

et là magie ça marche.
Je ne sais pas pourquoi ils n'ont jamais corrigé ce problème de l'inférence de type.

Et par contre au sujet de :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 
val f : 'a -> () = <fun>

je ne connais qu'une seule fonction en caml qui aie ce type là (qui ne dépende pas de variable externes et sans effets de bords) et elle s'appelle ignore donc ce type n'est pas le polymorphisme, c'est une ignominie venue du monde des langages non typés où l'on a le droit de demander le type d'un objet (excepté pour la fonction ignore qui mathématiquement ce traduit par toute proposition implique vrai, à ben oui et la proposition on a rien à foutre, d'où le nom ignore, ça ne peut être que le sens d'une telle fonction).

[gasche]

Non, ce que tu dis n'est pas exact.

ça c'est le vieux bug caml. Il ne sait pas que f x = g x est la même chose que f = g (si l'on est sur que ce sont des fonctions)
[...]
Je ne sais pas pourquoi ils n'ont jamais corrigé ce problème de l'inférence de type.

Ça n'est pas un bug, ça n'est pas un problème. C'est nécessaire. Dans un langage impur, il est tout simplement faux de dire que "f x = g x" et "f = g" sont équivalents. C'est expliqué dans ce post : on peut construire des fonctions pour lesquelles ce n'est pas vrai.

Donc si on "corrigeait ce problème" comme tu dis, on pourrait faire sauter le système de typage de OCaml avec de purs termes OCaml (pas de magie, juste un effet de bord). Ce qui revient à le détruire.


De plus, ta modification de mon exemple ne "corrige pas un problème". J'ai montré que si on construit une valeur du type ('a, 'b) apply, elle n'est pas polymorphe (ce qui est clair). Tu as montré que si on construisait une nouvelle valeur à chaque fois, le tout étaitt polymorphe. C'est clair, mais ce n'est pas ce que je veux. Et d'ailleurs la deuxième version, poly_app, où ça marche alors qu'on ne construit encore qu'une seule valeur, montre bien que le comportement que je cherche est possible, et illustre le polymorphisme de second ordre.


Par ailleurs je ne vois pas ton problème au sujet de ignore. Cette fonction n'est pas ignoble et on peut la définir dans un langage fonctionnel pur : (fun _ -> ()). En quoi est-une ignominie ? Évidemment son type n'est pas très intéressant, mais celui de (fun x -> x) non plus et pourtant c'est une très jolie fonction !

[NokyDaOne]

Non, ce que tu dis n'est pas exact.



Ça n'est pas un bug, ça n'est pas un problème. C'est nécessaire. Dans un langage impur, il est tout simplement faux de dire que "f x = g x" et "f = g" sont équivalents. C'est expliqué dans ce post : on peut construire des fonctions pour lesquelles ce n'est pas vrai.

Donc si on "corrigeait ce problème" comme tu dis, on pourrait faire sauter le système de typage de OCaml avec de purs termes OCaml (pas de magie, juste un effet de bord). Ce qui revient à le détruire.

Effectivement, je n'avais jamais vu les choses sous cet angle. Saleté d'effets de bord.

Par ailleurs je ne vois pas ton problème au sujet de ignore. Cette fonction n'est pas ignoble et on peut la définir dans un langage fonctionnel pur : (fun _ -> ()). En quoi est-une ignominie ? Évidemment son type n'est pas très intéressant, mais celui de (fun x -> x) non plus et pourtant c'est une très jolie fonction !

Non je n'ai rien contre la fonction ignore qui est parfois bien utile (j'ai vu des fonctions avec des retours qui ne servent à rient parfois).
C'est juste que j'ai vu des gens programmer avec des fonctions du type 'a -> unit et qui n'étaient pas des fonctions ignore (pas en caml bien sûr, mais en des langages avec introspection) et qui osaient appeler ça du polymorphisme.

[SpiceGuid]

Dans le genre fonction ignoble démasquée par son type tu peux difficilement faire pire que failwith :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# failwith;;
- : string -> 'a = <fun>

Ça n'est pas un bug, ça n'est pas un problème. C'est nécessaire. Dans un langage impur, il est tout simplement faux de dire que "f x = g x" et "f = g" sont équivalents.

Le polymorphisme faible n'existe pas en F#, je me demande bien comment le problème est résolu, est-ce que c'est un effet bénéfique du mot clé mutable qui remplace la fonction ref ?

[gasche]

Le polymorphisme faible n'existe pas en F#

Je doute fortement de cette affirmation.

Est-ce la goutte qui me forcera finalement à installer Mono pour vérifier, m'exposant tragiquement aux foudres judiciaires d'une bande de requins ? Quelle injustice.

Je sais que le système de typage de F# fait la différence entre les "fonctions pures" et les "fonctions avec des trucs louches devant" (let f x = ..., let f = let .. in fun x -> ...). À partir de là, le problème du polymorphisme faible est peut-être formulé autrement, mais ça n'explique pas comment ils typeraient quelque chose comme "let truc = ref []".


PS : let rec failwith (s : string) = failwith s
(pourquoi est-ce que les gens trouvent tout à fait normal que le main de Haskell soit typé IO (), mais trouvent failwith ignoble ? Au niveau du typage c'est la même chose)

[alex_pi]

Le polymorphisme faible n'existe pas en F#, je me demande bien comment le problème est résolu, est-ce que c'est un effet bénéfique du mot clé mutable qui remplace la fonction ref ?

Je n'ai aucune idée de ce qu'il se passe en F#, mais ton explication ne saurait être la bonne puisqu'en OCaml, il n'y a de base que le mot clé mutable, et que le type 'a ref est ensuite défini par

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

type 'a ref = {mutable content : 'a}

et que := et ! sont ensuite facilement définie dessus.

[LLB]

Le polymorphisme faible existe en F#. Les exemples donnés sur l'autre page ont exactement le même comportement en F# (le compilateur parle de "Value restriction").

Par ailleurs je ne vois pas ton problème au sujet de ignore. Cette fonction n'est pas ignoble et on peut la définir dans un langage fonctionnel pur

Le type unit et la fonction ignore ont peu d'intérêt, si on ne fait pas d'effet de bord.

en OCaml, il n'y a de base que le mot clé mutable, et que le type 'a ref est ensuite défini par

C'est exactement pareil pour F#. Les fonctions ref, (:=) et (!) sont définies de la même fonction qu'en Caml. Le seul truc en plus, c'est que l'on peut écrire :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

let mutable a = 3

Mais cela ne change pas grand-chose. Il y a une restriction sur a (on ne peut pas y accéder dans une closure). Cette construction existe par compatibilité avec C# (on peut ensuite passer a en référence à une fonction) et - j'imagine - pour des raisons de performances

[alex_pi]

Le type unit et la fonction ignore ont peu d'intérêt, si on ne fait pas d'effet de bord.

Pour le type unit, ca a peu d'intéret (a priori) en valeur de retour, mais ca peut être tres intéressant en valeur d'entrée pour créer une suspension, si on est sur qu'elle sera forcée zéro ou une fois (si plus, il vaut mieux faire du lazy, mais parfois c'est sortir un marteau pillon pour écraser une mouche).

Et même en Haskell, faire un calcul dont on ne regarde pas la valeur de retour peut même avoir un intéret ! Parce que des effet de bords sont cachés dans la paresse. Il peut parfois être intéressant de forcer une suspension "quand on a du temps" pour qu'elle soit ensuite utilisable très rapidement quand on a "moins de temps".

[gasche]

Le type unit et la fonction ignore ont peu d'intérêt, si on ne fait pas d'effet de bord.

Je comprends ce que tu veux dire mais attention, on peut chipoter ! Le type unit est un type respectable (oui monsieur) et on peut lui trouver des qualités théoriques certaines.

Par exemple, on est habitué de nos jours aux types algébriques "simples" qui n'ont pas d'arguments. Mais comment on fait dans un modèle spartiate où ça n'existe pas ?
On fait avec (type 'a option = Some of 'a | None of unit)

Plus généralement, "unit" incarne le type par excellence qui n'apporte pas d'informations. Et, même si c'est surtout utile en cas d'effet de bord ("des valeurs ont été modifiées, circulez, il n'y a plus rien à voir"), ça peut aussi servir dans un contexte fonctionnel pur.
Par exemple si j'ai une série de "producteurs" (type ('a, 'b) prod = 'a -> 'b), et j'ai déclaré tout un tas de fonctions auxiliaires cool dessus (composition, etc.), et je veux des producteurs "constants", ie. qui peuvent produire sans qu'on leur donne aucune information. unit !


Edit : alex_pi : je ne pense pas qu'on puisse écrire une fonction forçant l'évaluation et qui termine, dans un langage fonctionnel pur.

[LLB]

OK, je suis d'accord avec ça. Je pensais à unit comme type de retour, mais vous avez raison. :-)

[alex_pi]

Edit : alex_pi : je ne pense pas qu'on puisse écrire une fonction forçant l'évaluation et qui termine, dans un langage fonctionnel pur.

J'avoue ne pas comprendre. On peut quand même forcer une suspension, non?

[gasche]

Si tu définis type 'a suspension = unit -> 'a, alors oui évidemment. Je croyais que tu parlais aussi de `seq` et consorts : je ne connais pas d'implémentation "pure" de seq (la première idée, let force x = let bot = bot in if x == bot then x else x , ne termine pas); l'intuition dit qu'il n'en existe pas, mais il est possible que d'autres innocentes fonctionnalités du langage permettent de contourner cette interdiction, je ne sais pas.

Par contre (ce n'est pas vraiment lié mais c'est rigolo et cela utilise unit), on peut implémenter le "call with current continuation" en utilisant uniquement unit et un effet de bord, ce qui est plutôt amusant.

[alex_pi]

Je ne comprends toujours pas... Effectivement, si tu as un programme fonctionnel pur a evaluation strict, il ne doit pas être possible d'encoder soit même la paresse a la main (puisque le fait de forcer une fois une suspension a un effet de bord, a savoir que de forcer cette suspension ailleurs doit se faire en O(1)). Mais moi je parlais d'un langage avec paresse (systématique à la Haskell ou optionnelle à la OCaml), et là on peut bien sûr forcer une suspension et rejeter le résultat. Si le langage est pur, ça n'aura pas d'impact au niveau algorithmique (le résultat), mais ça aura bien un impact au niveau de la complexité. C'est d'ailleurs ce qui fait dire aux gens qu'Haskell est un langage dans lequel il peut être extremement complexe de se faire une idée fiable de la complexité d'un programme