Theorème de Curry

◮ Pour les fonctions a plusieurs parametres, nous avons vu 2 notations: # let f1 = function x -> function y -> x + y;; val f1 : int -> int -> int = <fun>
# let f2 = function (x,y) -> x + y;; val f2 : int * int -> int = <fun>
◮ Quelle notation privil´egier?
f1 : E × F → G (x, y) 7−→ f (x, y)
f2 : E → F → G x 7−→ y 7−→ (f x y)
Définition (Currification) Technique transformat une fonction prenant un n-uplet en entr´ee en une composition de fonctions prenant chacune un seul argument en entr´ee.
◮ Ce theoreme peut se voir comme un isomorphisme entre fonctions (isomorphisme de Curry-Howard) ◮ NB: tout langage utilisant la notion de fermeture peut manipuler des fonctions currifi´ees
◮ Currification / decurrification en Caml: # let curry = function f -> function x -> function y -> f (x,y);;
# let uncurry = function f -> function pair -> (f (fst pair) (snd pair));;
◮ Typage de ces fonctions ? ◮ Interet de la currification: • application fonctionnelle ramenée a un mécanisme uniforme (évaluation d’un paramètre)