Envoyé par
Diakt
p g x y -> p (g(x),y)
Donc x est appliqué à g :
g = x -> 'a
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 :
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 *)
Puis y appliqué à p :
y = p -> 'b
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 :
Où 'a est le type retourné par g lorsqu'on applique avec un élément x de type 'x.
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 :
<fun> : 'p -> 'g -> 'x -> 'y -> 'b
en substituant ce qu'on sait :
<fun> : (('a * 'y) -> 'b) -> ('x -> 'a) -> '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.
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.
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 ?
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.
Aussi imaginons cette formule: ('a->'b)-> ('c->'d)
Est telle équivalente à : ('b->'a) -> ('d->'c) ?
Ces deux formulations sont en effet "alpha-équivalentes", puisqu'on peut passer de l'une à l'autre avec un renommage correct.
Ainsi :
est équivalent à
mais n'est pas équivalent à :
'x -> 'x -> 'z (* car ici, le type des deux paramètres DOIT être le même *)
ni à :
('x -> 'y) -> 'z (* car ici, on force le premier paramètre a être une fonction *)
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.
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 :
f : 'a -> (b -> 'c) -> 'c -> 'a
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."
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 :
1 2 3 4
| f : 'a -> (b -> 'c) -> 'c -> 'a
x : bool
g : b -> int
f x g : ??? |
D'après toi, quel est le type de "f x g" ?
Partager