Curry

Currying (din engleză currying , uneori - currying ) - transformarea unei funcții din mai multe argumente într-un set de funcții, fiecare dintre acestea fiind o funcție a unui argument. Posibilitatea unei astfel de transformări a fost observată pentru prima dată în scrierile lui Gottlob Frege , studiat sistematic de Moses Scheinfinkel în anii 1920 și numit după Haskell Curry , dezvoltatorul logicii combinatorii , în care reducerea la funcții ale unui argument este fundamentală.

Definiție

Pentru o funcție de două argumente , operatorul curry efectuează o conversie - ia un argument de tip și returnează o funcție de tip . Intuitiv, curry o funcție vă permite să remediați unele dintre argumentele acesteia, în timp ce returnați funcția din argumentele rămase. Astfel, este o funcție de tip . $h\colon (A\times B)\la C$ $\lambda$ $\Lambda (h)\colon A\to (B\to C)$ $A$ $(B\la C)$ $\lambda$ $(A\time B\la C)\la (A\la (B\la C))$

Decurrying ( eng. uncurring ) este introdus ca o transformare inversă - restabilirea argumentului curred: pentru o funcție, operatorul decurringrealizează transformarea; tipul operatorului decurry este. $k\colon A\la (B\la C)$ $\epsilon$ $\epsilon (k)\colon A\times B\to C$ $(A\la (B\la C))\la (A\times B\to C)$

În practică, currying vă permite să luați în considerare o funcție care nu a primit toate argumentele furnizate. Operatorul curry este încorporat în unele limbaje de programare pentru a permite funcționarea funcțiilor cu mai multe locuri, cele mai comune exemple de astfel de limbaje fiind ML și Haskell . Toate limbile care acceptă închideri vă permit să scrieți funcții curriculate.

Punct de vedere matematic

În informatică teoretică , currying oferă o modalitate de a examina funcțiile mai multor argumente în cadrul unor sisteme teoretice foarte simple, cum ar fi calculul lambda . În teoria mulțimilor, currying este o corespondență între mulțimi și . În teoria categoriilor, currying provine din proprietatea universală a exponenţialului ; în situația unei categorii carteziane închise , aceasta conduce la următoarea corespondență. Există o bijecție între seturi de morfisme dintr-un produs binar și morfisme într-un exponențial care este natural în raport cu și în raport cu . Această afirmație este echivalentă cu faptul că functorul produs și functorul Hom sunt functori adjuncți. $C^{A\times B}$ $\left(C^{B}\right)^{A}$ $f\colon (X\time Y)\to Z$ $g\colon X\la Z^{Y}$ $X$ $Z$

Aceasta este o proprietate cheie a unei categorii carteziane închise sau, mai general, a unei categorii monoidale închise . Prima este suficientă pentru logica clasică, dar a doua este o bază teoretică convenabilă pentru calculul cuantic . Diferența este că produsul cartezian conține doar informații despre o pereche de două obiecte, în timp ce produsul tensor utilizat în definirea unei categorii monoidale este potrivit pentru descrierea stărilor încurcate [1] .

Din punctul de vedere al corespondenței Curry-Howard , existența funcțiilor currying (tipul de locuibilitate și decurrying (tipul de locuibilitate ) este echivalentă cu o afirmație logică ( tipul de produs corespunde conjuncției , iar tipul funcțional implicației ). sunt continue după Scott . $((A\times B)\la C)\la (A\la (B\la C)$ $(A\la (B\la C)\la ((A\times B)\la C)$ $((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))$ $A\ori B$ $A la B$

Curry din punct de vedere al programării

Currying-ul este utilizat pe scară largă în limbaje de programare , în primul rând cele care suportă paradigma de programare funcțională . În unele limbi, funcțiile sunt aplicate în mod implicit, adică funcțiile cu mai multe locuri sunt implementate ca funcții de un singur loc de ordine superioară , iar aplicarea argumentelor la acestea este o secvență de aplicații parțiale .

Limbajele de programare cu funcții de primă clasă definesc de obicei operațiuni curry(traducerea unei A, B -> Cfuncții de semnătură de vizualizare într-o funcție de semnătură A -> B -> C) și uncurry(efectuarea transformării inverse - maparea unei funcții de semnătură de vizualizare la o funcție cu A -> B -> Cdouă locuri a formularului A, B -> C). În aceste cazuri, legătura cu operația parțială a aplicației este transparentă papply: curry papply = curry.

Note

↑ Ioan c. Baez și Mike Stay, „ Physics, Topology, Logic and Computation: A Rosetta Stone Archived 15 May 2013 at the Wayback Machine ”, (2009) ArXiv 0903.0340 Arhivat la 20 iulie 2014 la Wayback Machine in New Structures for Physics , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlin, 2011, p. 95-174.

Literatură

Benjamin Pierce. Tipuri în limbaje de programare / Per. din engleză: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 p. — ISBN 978-5-7913-0082-9 .
Teoria tipurilor // Homotopy Teoria tipurilor: Fundamentele univalente ale matematicii . - Princeton : Institutul pentru Studii Avansate , 2013. - 603 p.