Version imprimable
Bonjour à tous.
Aprés avoir chercher sans résultats concrêts, je viens vers vous, pour vous demander quelques petites explications sur la Curryfication.
Par exemple je ne comprends pas vraiment :
Comment peut on déduire le type de ces fonctions ?Code:
2
3
4
5
6
Nommons pour démarrer les types à éclaircir :Code:#fun p x y -> p ( x ( y ));;
Dans le code, x est appliqué à y, donc :Code:
2
3
Puis, p est appliqué avec le retour d'un appel de x, donc :Code:'x = 'y -> 'a (* où 'a est "frais", à déterminer *)
Enfin, ta fonction prend p, x, y et retourne le résultat de p, elle doit donc avoir pour type :Code:'p = 'a -> 'b (* où 'a est le même que précédemment, et 'b est "frais" à déterminer *)
En substituant les égalités ci-dessus, ce type devient :Code:'p -> 'x -> 'y -> 'b (* même 'b que précédemment *)
Ce qui est alpha-équivalent (cela signifie "équivalent à un renommage sain près") à :Code:('a -> 'b) -> ('y -> 'a) -> 'y -> 'b
Je te laisse le soin de faire le même petit exercice avec ta seconde fonction pour te convaincre que le type inféré est correct.Code:- : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>
Ceci étant, l'inférence de type a peu de rapport avec le sujet de la curryfication dont tu parlais.
---
La curryfication, c'est l'idée qu'une fonction qui attend plusieurs arguments est moralement équivalente à une fonction qui prendrait un argument et renverrait la fonction qui attendrait le reste des arguments afin de produire le même résultat.
En types OCaml, cela signifie que la fonction :
qui prend en argument une paire de deux éléments, est moralement équivalente à une fonction :Code:f : ('a * 'b) -> 'v
qui prendrait d'abord le premier de ces deux arguments, et retournerait une fonction qui attend le second argument 'b, et retourne le même résultat de type 'v.Code:f : 'a -> ('b -> 'v)
En pratique, on préfère écrire les fonctions sous la seconde forme : en effet, cela permet notamment de passer les arguments un par un ('a tout de suite, et 'b plus tard), et cela s'avère très pratique dans certaines situations. Si tu veux en savoir plus, ce principe de ne pas passer tous les arguments d'un coup s'appelle l'application partielle, et on a aussi un nom pour une fonction comme celle retournée (c'est-à-dire une fonction qui "retient" déjà un certain nombre de ses paramètres), on l'appelle une fermeture.
J'imagine qu'à la lumière de ces nouvelles choses tu dois avoir des questions, auxquelles nous nous ferons un plaisir de répondre. N'hésite pas à chercher des informations sur les termes apparaissant en gras dans mon message si tu veux creuser un peu plus le "pourquoi est-ce qu'on me parle de curryfication ? à quoi ça sert ?".
---
Note enfin que lorsque j'ai écrit :
C'est équivalent, par définition de "->" (on dit que "->" est associatif à droite, rien à voir avec la politique !), à :Code:f : 'a -> ('b -> 'v)
qui est aussi la forme du type de fonctions définies comme celles étudiées en début de ce message (fun a b -> ...).Code:f : 'a -> 'b -> 'v
Ainsi :
est une façon abrégée d'écrire :Code:(fun a b c -> foo)
Cette seconde façon de l'écrire souligne bien la curryfication : tu as bien une fonction qui prend un 'a et retourne une fonction qui prend un 'b et retourne une fonction qui prend un 'c et retourne foo.Code:(fun a -> (fun b -> (fun c -> foo)))
Dans un premier temps je te remercie de m'avoir éclairer sur le sujet :)
Effectivement détaillé comme cela, nous ne parlons pas de curryfication ici.
Donc pour le second exemple, ça me donnerais :
p g x y -> p (g(x),y)
Donc x est appliqué à g :
g = x -> 'a
Puis y appliqué à p :
y = p -> 'b
Puis p appliqué à ('a et 'b) :
P = ('a * 'b ) -> c (le signe * du à la virgule)
Et x -> 'd
Donc ma fonction prend p x y g comme arguments, et retourne le résultat de p, donc elle doit avoir le même type:
p g x y p me donne :
(('a * 'b ) -> c)) -> 'a -> 'd -> 'b -> 'c
Enfin je doute encore sur une question.
Imaginons notre fonction :
p g x p -> g(x(p),y)
Ma fonction prend donc les arguments g x p y et retourne le résultat de g non ?
Aussi imaginons cette formule: ('a->'b)-> ('c->'d)
Est telle équivalente à : ('b->'a) -> ('d->'c) ?
Car je ne comprends pas toujours la logique que choisit Ocaml pour déterminer 'a 'b 'c 'd, donc j'aimerais savoir si ils ont un ordre précis.
Attention, j'avais pris la peine de noter 'x le type de x. L'apostrophe indique que je ne parle pas d'un type concret, mais d'une variable de type qu'on va chercher à "raffiner" en voyant comment elle est utilisée. Ainsi, j'aurais écrit :Citation:
Envoyé par Diakt
Code:g = 'x -> 'a (* g prend un paramètre du type de x, et retourne un paramètre d'un certain type qu'on appellera 'a *)
Non ! Dans ton expression, p prend un unique paramètre, qui est une paire composée de "g x" d'un côté, et "y" de l'autre. Ainsi, on a :Citation:
Puis y appliqué à p :
y = p -> 'b
Où 'a est le type retourné par g lorsqu'on applique avec un élément x de type 'x.Code:'p = ('a * 'y) -> 'b
Et donc ta fonction prend un p : 'p, un g : 'g, un x : 'x, un y : 'y, et retourne quelque chose du type de p (g(x),y), c'est-à-dire :
en substituant ce qu'on sait :Code:<fun> : 'p -> 'g -> 'x -> 'y -> 'b
Je te laisse essayer de comprendre cette signature. Il y a quatre paramètres, dont les deux premiers sont eux-même des fonctions.Code:<fun> : (('a * 'y) -> 'b) -> ('x -> 'a) -> 'x -> 'y -> 'b
Une remarque un peu plus "compliquée" tout de même : dans toutes les équations que j'ai données dans ce raisonnement, il n'y en a aucune qui contraigne 'a, 'b, 'x et 'y.
Cette fonction est valide quels que soient 'a, 'b, 'x et 'y. En particulier, 'b peut très bien être un type de la forme ('c -> d') ! Auquel cas, cela signifie que la fonction g qu'on obtient en paramètre attend effectivement plus d'un paramètre, et on ne lui en fournit qu'un dans notre fonction : ce serait un nouvel exemple d'application partielle.
Au regard du paragraphe précédent, tu devrais plutôt dire "et retourne le résultat de g appliqué à un argument ...", car g pourra tout aussi bien être une fonction qui attend un seul argument qu'une fonction qui en attend plusieurs.Citation:
Enfin je doute encore sur une question.
Imaginons notre fonction :
p g x p -> g(x(p),y)
Ma fonction prend donc les arguments g x p y et retourne le résultat de g non ?
Ces deux formulations sont en effet "alpha-équivalentes", puisqu'on peut passer de l'une à l'autre avec un renommage correct.Citation:
Aussi imaginons cette formule: ('a->'b)-> ('c->'d)
Est telle équivalente à : ('b->'a) -> ('d->'c) ?
Ainsi :
est équivalent àCode:'a -> 'b -> 'c
mais n'est pas équivalent à :Code:'x -> 'y -> 'z
ni à :Code:'x -> 'x -> 'z (* car ici, le type des deux paramètres DOIT être le même *)
Code:('x -> 'y) -> 'z (* car ici, on force le premier paramètre a être une fonction *)
L'important est de ne pas te focaliser sur la lettre choisie lorsque celle-ci est précédée d'une apostrophe. Pour lire une signature comme :Citation:
Car je ne comprends pas toujours la logique que choisit Ocaml pour déterminer 'a 'b 'c 'd, donc j'aimerais savoir si ils ont un ordre précis.
Tu peux dire : "Pour tout 'a, pour tout 'c, une fonction qui prend un paramètre de type 'a, un autre paramètre de type (b -> 'c), et un troisième paramètre de type 'c, et retourne un résultat de type 'a."Code:f : 'a -> (b -> 'c) -> 'c -> 'a
Note que je n'ai pas dit "pour tout b", car b n'est pas précédé d'une apostrophe, ce serait donc un type qui existe dans ton code ("type b = ...").
Ce qui importe par contre, c'est de voir les multiples occurences du même 'x. Dans la signature présentée ci-dessus, les deux occurences de 'a représentent le même type. De même, les deux occurences de 'c représentent le même type.
Cela implique quelque chose sur le typage d'une application partielle, et devrait te permettre de déterminer le type "???" dans ce problème, si tu as bien compris :
D'après toi, quel est le type de "f x g" ?Code:
2
3
4
Je te remercie de toutes tes explications détaillées, dorénavant les types des fonctions n'ont pratiquement plus de secrets pour moi. Même si cependant, ton exemple d'application partielle me laisse perplexe.
Je peux tout de même dire que :
f est une fonction qui prends trois paramètres et retourne un type 'a.
Ainsi que les deux 'a sont de même type. Idem pour les deux 'c
Soit, pour f: 'a -> (b->'c)Donc si type b est un int, 'c de type int,Citation:
qui prendrait d'abord le premier de ces deux arguments, et retournerait une fonction qui attend le second argument 'b, et retourne le même résultat de type 'v.
Et ainsi que x : type bool
Signifie que (b->'c) est de type bool.
Donc (f x g) nous retournera un type bool.
Mais je ne reste pas convaincu de cette démonstration..
C'est correct.Citation:
f est une fonction qui prends trois paramètres et retourne un type 'a.
Oui, si le même symbol apparaît plusieurs fois, il représente le même type.Citation:
Ainsi que les deux 'a sont de même type. Idem pour les deux 'c
Là je ne te suis plus. f a pour type 'a -> (b -> 'c) -> 'c -> 'a.Citation:
Soit, pour f: 'a -> (b->'c)
b est un type (puisqu'il n'est pas précédé d'une apostrophe). Donc un b est un b, rien d'autre (tout comme un int est un int). :)Citation:
Donc si type b est un int
Le reste de ton raisonnement n'est pas correct.
Voici comment raisonner :Code:
2
3
4
5
Que faut-il remarquer ici ?Code:
2
3
4
5
6
Le premier 'a a été mangé, puisqu'on a donné un (x : bool) à la fonction f. De ce fait, on en déduit que dans la fonction retournée par (f x), ce qui auparavant pouvait être "nimporte quel 'a" doit désormais être du même type que x, c'est-à-dire bool. C'est pourquoi le type 'a retourné au final est bool dans cette application partielle.
Continuons :
Ici, on a passé (g : b -> int) en argument de (f x : (b -> 'c) -> 'c -> bool). b est bien égal à b, jusqu'ici tout va bien. Et toutes les occurences de 'c doivent être remplacées par int, conformément au type de g. D'où (f x g : int -> bool).Code:
2
3
4
5
6
Pour raisonner avec ces types, dans un premier temps il faut vraiment que tu imagines "unifier" le type attendu par la fonction avec le type que tu fournis.
Si les deux types sont monomorphes (comme "b", "int -> bool"), alors ils doivent être égaux :
Si un des deux types seulement est polymorphe, alors toutes ses occurences doivent être remplacées par le type monomorphe de l'autre côté :Code:
2
3
4
5
6
7
8
Si les deux types sont polymorphes, alors pour unifier les deux types il suffit de renommer l'un avec la lettre de l'autre (avec un nom neuf comme 'z pour éviter les collisions) :Code:
2
3
4
5
6
7
8
9
Il est normal que ça puisse paraître bien compliqué.Code:
2
3
4
5
6
7
8
Imagine un robot polymorphe, qui a deux bras qui attendent un objet, et qui te rend l'objet de son bras gauche. Ce robot tend toujours le bras gauche en premier :
Maintenant, si tu appliques partiellement ce robot en lui tendant un objet de type (mapomme : pomme), il te reste un :Code:robot : 'brasgauche -> 'brasdroit -> 'brasgauche
C'est un robot qui tend son bras droit, et retournera une pomme. Puisque tu lui as passé une pomme, et qu'il retourne quelque chose du type de ce qu'on lui passe en premier, alors à présent il retournera forcément une pomme ! :)Code:robot mapomme : 'brasdroit -> pomme
Mais si tu as deux des ces robots, et qu'ils sont capables de supporter leur propre poids, peut-être que tu auras envie de tenter cela :
Puisque tu lui as passé un robot, il te rendra un robot après que tu lui donnes quelque chose à mettre dans sa main droite. Tu remarqueras aussi que le type 'brasdroit1 n'est pas égal au type 'brasdroit2, après tout tu peux bien passer quelque chose différent à l'autre robot.Code:robot robot : 'brasdroit1 -> ('brasgauche2 -> 'brasdroit2 -> 'brasgauche2)
Je ne sais pas si ça aide à se faire une idée de ce qu'il se passe maintenant que je l'ai écrit :mrgreen:
Bon courage pour comprendre cela, ça semble dur mais une fois que tu auras compris tu verras que c'est vraiment facile (tellement facile qu'OCaml fait tous ses calculs de type pour toi).
Hey bien ! Merci pour tout ces "petites" notions forte intéressantes !
Notamment pour les applications partielles qui me paraissent maintenant plus clair avec tes explications.
J'ai bien aimé celle du robot ;)
Merci encore de m'avoir donner de ton temps pour me familiariser d'avantage avec la programmation fonctionnelle, je commence à voir maintenant pourquoi elle est dans le cursus universitaire 8-)
En fait ce n'est pas éloigné de ce que les gens connaissent déjà sous le nom "résoudre une équation". Pendant l'inférence, les variables de types se comportent comme des inconnues, sur lesquelles on apprend des choses (des égalités entre types).Citation:
Il est normal que ça puisse paraître bien compliqué.
Par exemple si je sais que (f : 'a -> 'a) (lire "f est de type 'a -> 'a") et que (x : int), en voyant (f x) je déduis que ('a = int). On peut voir tout ça comme un système d'équations à résoudre; quand on apprend que l'inconnue 'a est égale à la constante int, on peut remplacer 'a partout par int, c'est naturel.
Une difficulté éventuelle par rapport à ce que les gens ont vu en mathématique est l'introduction régulière de nouvelles inconnues : si je sais que (f : 'v) et que je lis (f x), j'en déduis que f doit être une fonction, donc 'v est un type flèche: j'introduis deux nouvelles inconnues, mettons 'v1 et 'v2, avec l'équation 'v = ('v1 -> 'v2).
(C'est juste une méta-remarque sur l'excellente explication de Ptival, pas une critique. Merci Diak au passage pour tes remerciements; ils ne me sont pas adressés mais je sais que c'est agréable à lire : quand on explique quelque chose c'est plus motivant de recevoir en retour "merci, ça me pousse à m'intéresser au domaine" que rien du tout ou seulement "merci j'ai pu résoudre mon exercice".)
Oui, à la seule différence qu'on ne doit pas en "rétro-conclure" que (f : int -> int). Les équations/contraintes arrivent lorsqu'on commence à appliquer une fonction, mais la fonction initiale conserve son type généralisé, et peut adopter un type spécialisé différent dans un autre contexte.Citation:
Envoyé par gasche
C'est un peu cette idée que je voulais faire passer avec mon robot. :mouarf:
L'idée c'est que lorsque dans un début d'application, on déduit que ('a = int), alors dans la suite de l'application on ne peut plus briser cette équation. Mais dans une autre application, peut-être que ('a = float), ou ('a = 'b), et dans certains cas, ('a = 'b -> 'c) !
Il y a une subtilité là-dessous qu'on ne peut pas cacher infiniment: il y a une différence entre variable (monomorphe) d'inférence et variable (polymorphe) d'un schéma de type. Mais quand on est en train d'inférer, on ne manipule pas de polymorphisme, on ne manipule que des variables d'unification ("inconnues"). Ici quand je dis que f a le type ('a -> 'a), dans un contexte d'inférence, ça veut dire que le type de cette occurence de f s'instancie ainsi, où la variable 'a est une variable fraîche d'unification.
Donc on peut expliquer l'inférence avec seulement des variables d'inférences. Le type final inféré contient des variables libres, et on passe sous tapis le fait de dire qu'elles sont généralisées (si c'est dans une définition avec 'let') pour devenir des variables de schéma.