Curry

Currying (från engelska currying , ibland - currying ) - omvandlingen av en funktion från många argument till en uppsättning funktioner, som var och en är en funktion av ett argument. Möjligheten till en sådan transformation noterades först i Gottlob Freges skrifter , systematiskt studerade av Moses Scheinfinkel på 1920-talet och uppkallad efter Haskell Curry , utvecklaren av kombinatorisk logik , där reduktion till funktioner av ett argument är grundläggande.

Definition

För en funktion av två argument utför curryoperatorn en konvertering - den tar ett typargument och returnerar en funktion av typ . Intuitivt, genom att currya en funktion kan du fixa några av dess argument samtidigt som funktionen returneras från de återstående argumenten. Alltså är en funktion av typ . $h\colon (A\times B)\to C$ $\lambda$ $\Lambda (h)\kolon A\to (B\to C)$ $A$ $(B\to C)$ $\lambda$ $(A\times B\to C)\to (A\to (B\to C))$

Decurrying ( eng. uncurring ) introduceras som en invers transformation - återställer curry-argumentet: för en funktionden decurry-operatortransformationen; typen av decurryoperatör är. $k\colon A\to (B\to C)$ $\epsilon$ $\epsilon (k)\colon A\times B\to C$ $(A\to (B\to C))\to (A\times B\to C)$

I praktiken låter currying dig överväga en funktion som inte fick alla de angivna argumenten. Curry-operatorn är inbyggd i vissa programmeringsspråk för att tillåta flerplatsfunktioner att curry, de vanligaste exemplen på sådana språk är ML och Haskell . Alla språk som stöder stängningar låter dig skriva curry-funktioner.

Matematisk synvinkel

Inom teoretisk datavetenskap ger currying ett sätt att undersöka funktioner hos flera argument inom mycket enkla teoretiska system som lambdakalkylen . I mängdteorin är currying en överensstämmelse mellan set och . I kategoriteorin kommer currying från exponentialets universella egenskap ; i situationen med en kartesisk sluten kategori leder detta till följande korrespondens. Det finns en bijektion mellan uppsättningar av morfismer från en binär produkt och morfismer till en exponentiell som är naturlig med avseende på och med avseende på . Detta påstående är ekvivalent med det faktum att produktfunktioner och Hom-funktioner är samverkande funktioner. $C^{A\times B}$ $\left(C^{B}\right)^{A}$ $f\colon (X\ gånger Y)\till Z$ $g\colon X\to Z^{Y}$ $X$ $Z$

Detta är en nyckelegenskap för en kartesisk sluten kategori , eller, mer allmänt, en sluten monoidal kategori . Den första är helt tillräcklig för klassisk logik, men den andra är en praktisk teoretisk grund för kvantberäkning . Skillnaden är att den kartesiska produkten endast innehåller information om ett par av två objekt, medan tensorprodukten som används i definitionen av en monoidal kategori är lämplig för att beskriva intrasslade tillstånd [1] .

Ur Curry-Howard-korrespondensens synvinkel är förekomsten av curryfunktioner (typ habitability och decurrying (typ habitability ) ekvivalent med ett logiskt påstående ( produkttyp motsvarar konjunktion och funktionell typ till implikation ). Currying och decurrying-funktioner är kontinuerliga enligt Scott . $((A\ gånger B)\to C)\to (A\to (B\to C)$ $(A\to (B\to C)\to ((A\times B)\to C)$ $((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))$ $A\ gånger B$ $A till B$

Skrämmande ur programmeringssynpunkt

Currying används ofta i programmeringsspråk , främst de som stöder det funktionella programmeringsparadigmet . På vissa språk är funktioner curry som standard, det vill säga flerplatsfunktioner implementeras som enplatsfunktioner av högre ordning , och appliceringen av argument på dem är en sekvens av partiella applikationer .

Programmeringsspråk med förstklassiga funktioner definierar vanligtvis operationer curry(översätta en vysignaturfunktion A, B -> Ctill en signaturfunktion A -> B -> C) och uncurry(utföra den omvända transformationen - mappa en vysignaturfunktion till en A -> B -> Ctvåställsfunktion av formuläret A, B -> C). I dessa fall är kopplingen till den partiella applikationsoperationen transparent papply: curry papply = curry.

Anteckningar

↑ John c. Baez och Mike Stay, " Physics, Topology, Logic and Computation: A Rosetta Stone Archived 15 May 2013 at the Wayback Machine ", (2009) ArXiv 0903.0340 Arkiverad 20 juli 2014 på Wayback Machine in New Structures for Physics , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlin, 2011, sid. 95-174.

Litteratur

Benjamin Pierce. Typer i programmeringsspråk / Per. från engelska: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 sid. — ISBN 978-5-7913-0082-9 .
Typteori // Homotopy Type Theory: Univalent Foundations of Mathematics . - Princeton : Institute for Advanced Study , 2013. - 603 sid.