J'ai juste un doute sur les deux dernières lignes: commit et merge sont bien des fonctions prenant les 2 premiers éléments en paramètre et faisant un résultat du type du dernier élément ?
Plus ou moins. La réponse de barmic est plus proche de la vérité, et c'est effectivement une pratique courante en programmation fonctionnelle (connue sous le nom de curryfication). Si j'écris le type de commit avec des parenthèses, cela donne :
valcommit:patch->(state->state)
C'est une fonction qui prend un patch et retourne une fonction des états dans les états. Pour prendre une notation utilisée en mathématiques, il faudrait prendre la notation indicée. commit décrit une famille de fonctions indexées par des patchs. Ce qui correspond bien à ce qu'exprime le diagramme :
Les flèches entre sommets sont des transformations indexées par des patchs. Lorsque j'ai écrit :
A = commit p O
il faudrait lire (en rajoutant des parenthèses) :
A = (commit p) O
soit la fonction commit p appliquée à O, ou avec des indices :
De la même manière, une suite de fonctions (f_{n})_{n \in \mathbb{N}} des réels dans les réels a pour type nat -> real -> real.
Il y a bien une correspondance entre cette approche à la Curry et celle où les fonctions prennent un couple. Elle traduit cette égalité algébrique :
L'exponentiel de l'exponentiel est égale à l'exponentiel du produit. C'est liée à l'algèbre des types : là où le produit cartésien correspond au produit, le type des fonctions correspond à l'exponentiel.
Si un type A a 2 éléments et un type B a 3 éléments, alors le type A -> B a 3^2 = 9 éléments (A -> B = B ^ A).
Pour en revenir à la fonction commit, elle associe chaque patch à une fonction des états sur eux-mêmes. Lorsque l'on dit que l'on applique un patch, c'est un abus de langage, en réalité on applique la fonction associée au patch via commit. Et lorsque l'on dit que les patchs sont associatifs, c'est parce que la composition de fonctions est associative. En notant . la composition de fonction on a les égalités :
(commit r . commit q) . commit p
= commit r . (commit q . commit p)
= commit r . commit q . commit p
Ce qui revient à « appliquer » les patchs dans l'ordre p, q, r.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Exemples concrets?
Posté par kantien . En réponse à la dépêche Pijul, contrôle de version et théorie des patchs, version 0.12. Évalué à 5. Dernière modification le 01 mai 2019 à 14:43.
Plus ou moins. La réponse de barmic est plus proche de la vérité, et c'est effectivement une pratique courante en programmation fonctionnelle (connue sous le nom de curryfication). Si j'écris le type de
commitavec des parenthèses, cela donne :C'est une fonction qui prend un patch et retourne une fonction des états dans les états. Pour prendre une notation utilisée en mathématiques, il faudrait prendre la notation indicée.
commitdécrit une famille de fonctions indexées par des patchs. Ce qui correspond bien à ce qu'exprime le diagramme :Les flèches entre sommets sont des transformations indexées par des patchs. Lorsque j'ai écrit :
A = commit p Oil faudrait lire (en rajoutant des parenthèses) :
A = (commit p) Osoit la fonction
commit pappliquée àO, ou avec des indices :De la même manière, une suite de fonctions (f_{n})_{n \in \mathbb{N}} des réels dans les réels a pour type
nat -> real -> real.Il y a bien une correspondance entre cette approche à la Curry et celle où les fonctions prennent un couple. Elle traduit cette égalité algébrique :
L'exponentiel de l'exponentiel est égale à l'exponentiel du produit. C'est liée à l'algèbre des types : là où le produit cartésien correspond au produit, le type des fonctions correspond à l'exponentiel.
Si un type A a 2 éléments et un type B a 3 éléments, alors le type
A -> Ba3^2 = 9éléments (A -> B = B ^ A).Pour en revenir à la fonction
commit, elle associe chaque patch à une fonction des états sur eux-mêmes. Lorsque l'on dit que l'on applique un patch, c'est un abus de langage, en réalité on applique la fonction associée au patch viacommit. Et lorsque l'on dit que les patchs sont associatifs, c'est parce que la composition de fonctions est associative. En notant.la composition de fonction on a les égalités :Ce qui revient à « appliquer » les patchs dans l'ordre
p, q, r.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.