Curryfication

# Curryfication

Posté par Aluminium95 le 23 novembre 2016 à 16:06. En réponse au journal Tagless-final ou l'art de l'interprétation modulaire.. Évalué à 1.
Bonjour !
Avant tout je voudrais te remercier pour ce super journal, instructif et très pédagogique (ce qui a certainement demandé beaucoup de temps de ta part).

Une modeste contribution pour la curryfication (il faut voir si c'est instructif ou non).

Une fonction est caractérisée par un ensemble de définition (son domaine), un ensemble d'arrivée (son codomaine) et une relation univoque entre un élément du domaine vers un élément du codomaine. Lorsque l'on traite des fonctions de plusieurs variables, le domaine est constitué de n-uplets ou tuples. Le principe de la curryfication consiste à se ramener, dans ce cas, à des fonctions d'une seule variable.

Il est dommage de construire directement des exemples dans des langages (ocaml/python) qui traitent les fonctions comme des valeurs directement. En langage mathématique, la distinction est plus nette et il est à mon avis plus lisible de comparer A ×ばつ B -> C et A -> EncodeFonction(B,C), avec A, B, C et EncodeFonction(B,C) qui sont des ensembles « normaux ».

Cela revient à dire :
```
A ×ばつ B -> C =~= A -> EncodeFonction (B,C)
```
En théorie des ensembles on écrit souvent B^C pour parler de cet objet qui encode une fonction de B vers C.

En python ou en caml, on ne travaille jamais vraiment avec des fonctions, mais toujours avec des codes qui représentent ces fonctions (ordinateur oblige), ainsi, la traduction est « déjà faite », et il suffit de produire une « fonction python ». L'égalité devient
```
EncodeFonction (A ×ばつ B, C) === EncodeFonction (A, EncodeFonction (B,C))
```
La transformation se fait très naturellement par la suite, et de manière générique (naturelle) en B,
```
def bijection (codeFonction1):
 codeFonction2 = lambda a: (lambda b: codeFonction(a,b)) # dans EncodeFonction (A, EncodeFonction (B,C))
 return codeFonction2
```
Notons que cela se base sur la capture d'arguments (l'argument a est utilisable dans la fonction dont l'argument est b).
Cette construction est un cas particulier d'adjonction.

# Curryfication