Question sur la curryfication

[Trap D]

Bonjour

Une question "théorique" me tracasse depuis quelque temps :
Imaginons le prédicat Prolog suivant

Code :

1
2
3
extract(Liste1, Liste2, Element, Value) :-
  nth0(Ind, Liste1, Element),
  nth0(Ind, Liste2, Value).

Ce prédicat recherche l'index de Element dans Liste1 et va ensuite rechercher la valeur correspondant à cet Index dans Liste2.

Venons-en maintenant à ma question : si j'utilise ce prédicat dans un maplist qui est un prédicat Prolog qui permet d'appliquer une régle sur une liste afin éventuellement d'obtenir une liste résultat (un peu comme le map du Lisp), par exemple :

maplist(extract(Ensemble1, Ensemble2), ListeElements, ListeResultats)

peut-on parler de "curryfication" ?

[SpiceGuid]

Ce que ton exemple démontre c'est que :

• statiquement ton langage possède la notion d'application partielle d'une clause
• dynamiquement ton langage possède une notion de fermeture (une clause liée avec un environnement)

Tu n'as pas besoin de curryfication si tu possède déjà ces deux caractéristiques, la curryfication c'est la même chose avec en plus des types fonctionnels.

Tu n'en as pas besoin mais si ça t'intéresse quand même :

• selon moi la notion de curryfication c'est la présence d'une transformation naturelle (un morphisme de foncteur vers foncteur) de type (A × B → C) → (A → B → C)
• le plus convaincant ce serait d'exhiber un tel type à l'aide d'un dialecte Prolog typé (par exemple alpha-Prolog)
• d'une façon équivalente, si l'application était associative à gauche alors on pourrait dire que les clauses Prolog sont currifiées
• c'est une fausse piste d'argumenter sur le nombre de paramètres pour affirmer que l'on possède la curryfication, le nombre de paramètres est une notion largement illusoire comme le montre l'exemple ci-dessous où l'on applique 4 arguments à la fonction identité

Code Caml :

1
2
3
let id x = x 
in  id id (+) 1 2;;

[Trap D]

Merci de ton explication. J'y vois un peu plus clair.

[SpiceGuid]

La curryfication est aussi une notion de logique, pas seulement une notion de programmation.
Il y a une correspondance entre les types fonctionnels et les propositions logiques.
Le type (A × B → C) → (A → B → C) correspond à la proposition (A & B ⇒ C) ⇒ (A ⇒ B ⇒ C).

Cette proposition donne une sémantique pour la conjonction, qui est celle utilisée lors de la démonstration.
En effet, pour prouver que (A & B) ⇒ C est vrai :

• on suppose que A est vrai
• sous la condition que A est vrai on prouve que B ⇒ C
• tout cela revient à prouver que A ⇒ (B ⇒ C)

Derrière le nom barbare il y a une proposition qui ne fait que formaliser une pratique courante de la démonstration.

[gasche]

Remarque : pour une vision de plus haut niveau de la curryfication, au delà du traitement logique on peut la représenter dans un cadre catégorique, comme l'adjonction entre (* A) et (A =>), qui permet de passer de (X * A -> Y) à (X -> (A => Y)).
Ce n'est certainement pas le seul point de vue possible, mais il apporte un large spectre d'applications (à toutes les interprétations catégoriques des langages de programmation, par exemple).