Curry

In der Mathematik und Informatik bezeichnet Currying die Technik, eine Funktion, die mehrere Argumente entgegennimmt, in eine Folge von Funktionsfamilien zu übersetzen , von denen jede ein einzelnes Argument entgegennimmt.

Im prototypischen Beispiel beginnt man mit einer Funktion, die zwei Argumente entgegennimmt, eines aus und eines aus , und Objekte in erzeugt. Die curried Form dieser Funktion behandelt das erste Argument als Parameter, um eine Familie von Funktionen zu erzeugen. Die Familie ist so angeordnet , dass es für jedes Objekt in genau eine Funktion gibt , sodass für jedes in .${\displaystyle f:(X\times Y)\to Z}$${\displaystyle X}$${\displaystyle Y,}$${\displaystyle Z.}$${\displaystyle f_{x}:Y\to Z.}$${\displaystyle x}$${\displaystyle X,}$${\displaystyle f_{x}}$${\displaystyle y}$${\displaystyle Y}$${\displaystyle f_{x}(y)=f(x,y)}$

In diesem Beispiel wird die Funktion selbst zu einer Funktion, die als Argumente entgegennimmt und eine Funktion zurückgibt, die jedes Element auf eine andere Menge abbildet . Die korrekte Notation hierfür ist etwas umständlich. Die Funktion gehört zur Menge der Funktionen. Gleichzeitig gehört die Funktion zur Menge der Funktionen. Somit ist etwas, das auf eine andere Menge abbildet , vom Typ . Mit dieser Notation ist eine Funktion, die Objekte aus der ersten Menge entgegennimmt und Objekte aus der zweiten Menge zurückgibt. Man schreibt also . Dies ist ein eher informelles Beispiel; präzisere Definitionen von „Objekt“ und „Funktion“ folgen weiter unten. Diese Definitionen variieren je nach Kontext und nehmen unterschiedliche Formen an, abhängig von der zugrunde liegenden Theorie. ${\displaystyle {\mbox{curry}}}$${\displaystyle f}$${\displaystyle x}$${\displaystyle f_{x}.}$${\displaystyle f}$${\displaystyle (X\times Y)\to Z.}$${\displaystyle f_{x}}$${\displaystyle Y\to Z.}$${\displaystyle x}$${\displaystyle f_{x}}$${\displaystyle X\to [Y\to Z].}$${\displaystyle {\mbox{curry}}}$${\displaystyle {\mbox{curry}}:[(X\times Y)\to Z]\to (X\to [Y\to Z]).}$

Currying ist verwandt mit, aber nicht identisch mit partieller Anwendung . ^{[ 1 ] [ 2 ]} Das obige Beispiel kann zur Veranschaulichung der partiellen Anwendung verwendet werden; es ist ihr sehr ähnlich. Die partielle Anwendung ist die Funktion, die das Paar und als Argumente entgegennimmt und zurückgibt. Mit derselben Notation wie oben hat die partielle Anwendung die Signatur . So geschrieben, kann man sehen, dass die Anwendung adjungiert zu Currying ist. ${\displaystyle {\mbox{apply}}}$${\displaystyle f}$${\displaystyle x}$${\displaystyle f_{x}.}$${\displaystyle {\mbox{apply}}:([(X\times Y)\to Z]\times X)\to [Y\to Z].}$

Das Currying einer Funktion mit mehr als zwei Argumenten kann durch Induktion definiert werden.

Currying ist sowohl in praktischen als auch in theoretischen Kontexten nützlich. In funktionalen Programmiersprachen und vielen anderen ermöglicht es die automatische Verwaltung der Argumentübergabe an Funktionen und Ausnahmen . In der theoretischen Informatik erlaubt es die Untersuchung von Funktionen mit mehreren Argumenten in einfacheren theoretischen Modellen mit nur einem Argument. Der allgemeinste Anwendungsbereich des strengen Currying- und Uncurrying-Konzepts sind abgeschlossene monoidale Kategorien . Diese bilden die Grundlage für eine umfassende Verallgemeinerung der Curry-Howard-Korrespondenz von Beweisen und Programmen hin zu einer Korrespondenz mit vielen anderen Strukturen, darunter Quantenmechanik , Kobordismen und Stringtheorie . ^{[ 3 ]}

Das Konzept des Currying wurde von Gottlob Frege eingeführt [ ^{4 ] [ 5 ], von} Moses Schönfinkel weiterentwickelt [ ^{6 ] [ 5 ] [ 7 ] [ 8 ] [ 9 ] [ 10 ] [ 11 ] und von} Haskell Curry weiterentwickelt ^{[ 8 ] [ 10 ] [ 12 ] [ 13 ]} .

Uncurrying ist die duale Transformation zum Currying und kann als eine Form der Defunktionalisierung betrachtet werden . Es nimmt eine Funktion , deren Rückgabewert eine andere Funktion ist , und erzeugt eine neue Funktion , die die Argumente von sowohl als auch als Parameter entgegennimmt und als Ergebnis die Anwendung von und anschließend auf diese Argumente zurückgibt. Dieser Prozess kann iterativ wiederholt werden. ${\displaystyle f}$${\displaystyle g}$${\displaystyle f'}$${\displaystyle f}$${\displaystyle g}$${\displaystyle f}$${\displaystyle g}$

Currying ermöglicht die Arbeit mit Funktionen, die mehrere Argumente entgegennehmen, und deren Verwendung in Kontexten, in denen Funktionen nur ein Argument benötigen. Beispielsweise lassen sich manche analytische Verfahren nur auf Funktionen mit einem einzigen Argument anwenden . In der Praxis benötigen Funktionen jedoch häufig mehr Argumente. Frege zeigte, dass es genügt, Lösungen für den Fall eines einzelnen Arguments bereitzustellen, da sich eine Funktion mit mehreren Argumenten in eine Kette von Funktionen mit jeweils einem Argument transformieren lässt. Diese Transformation ist der Prozess, der heute als Currying bekannt ist. ^{[ 14 ]} Alle „gewöhnlichen“ Funktionen, die typischerweise in der mathematischen Analysis oder in der Programmierung vorkommen , können curryt werden. Es gibt jedoch Kategorien, in denen Currying nicht möglich ist; die allgemeinsten Kategorien, die Currying erlauben, sind die abgeschlossenen monoidalen Kategorien .

Einige Programmiersprachen verwenden fast immer Curry-Funktionen, um mehrere Argumente zu verarbeiten; bekannte Beispiele sind ML und Haskell , wo in beiden Fällen alle Funktionen genau ein Argument haben. Diese Eigenschaft stammt vom Lambda-Kalkül , wo Funktionen mit mehreren Argumenten üblicherweise in Curry-Form dargestellt werden.

Currying ist verwandt mit, aber nicht identisch mit partieller Anwendung . ^{[ 1 ] [ 2 ]} In der Praxis kann die Programmiertechnik der Closures verwendet werden, um partielle Anwendung und eine Art von Currying durchzuführen, indem Argumente in einer Umgebung verborgen werden, die mit der curried Funktion übertragen wird.

Der Name „Curry“ in „Currying“ bezieht sich auf den Logiker Haskell Curry , der das Konzept ausführlich verwendete, doch Moses Schönfinkel hatte die Idee bereits sechs Jahre vor Curry. ^{[ 10 ]} Alternativ wurde die Bezeichnung „Schönfinkelisation“ vorgeschlagen. ^{[ 15 ]} Im mathematischen Kontext lässt sich das Prinzip auf Arbeiten von Frege aus dem Jahr 1893 zurückführen . ^{[ 4 ] [ 5 ]}

Der Ursprung des Begriffs „Currying“ ist unklar. David Turner gibt an, Christopher Strachey habe ihn 1967 in seinen Vorlesungsnotizen „ Fundamental Concepts in Programming Languages “ geprägt ^{[ 16 ].} In dieser Quelle wird das Konzept jedoch als „eine von Schönfinkel entwickelte Methode“ eingeführt, und der Begriff „Currying“ selbst wird nicht verwendet. Curry wird später im Zusammenhang mit Funktionen höherer Ordnung erwähnt ^{[ 7 ]} . John C. Reynolds definierte „Currying“ in einer Arbeit von 1972, beanspruchte aber nicht, den Begriff geprägt zu haben ^{[ 8 ] .}

Currying lässt sich am einfachsten anhand einer informellen Definition verstehen, die sich dann an verschiedene Anwendungsbereiche anpassen lässt. Zunächst müssen einige Notationen eingeführt werden. Die Notation bezeichnet alle Funktionen von nach . Ist eine solche Funktion , schreiben wir . Sei das geordnete Paar der Elemente von bzw. , also das kartesische Produkt von und . Hierbei können und Mengen, Typen oder andere Objekttypen sein, wie im Folgenden erläutert wird. ${\displaystyle X\to Y}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle f}$${\displaystyle f\colon X\to Y}$${\displaystyle X\times Y}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle X}$${\displaystyle Y}$

Gegeben sei eine Funktion

${\displaystyle f\colon (X\times Y)\to Z}$,

Currying erzeugt eine neue Funktion

${\displaystyle g\colon X\to (Y\to Z)}$Die

Das heißt, es nimmt ein Argument vom Typ entgegen und gibt eine Funktion vom Typ zurück . Es ist definiert durch ${\displaystyle g}$${\displaystyle X}$${\displaystyle Y\to Z}$

${\displaystyle g(x)(y)=f(x,y)}$

für vom Typ und vom Typ . Dann schreiben wir auch . ${\displaystyle x}$${\displaystyle X}$${\displaystyle y}$${\displaystyle Y}$

${\displaystyle {\text{curry}}(f)=g.}$

Das Entcurrying ist die umgekehrte Transformation und lässt sich am einfachsten anhand ihrer rechtsadjungierten Funktion verstehen.${\displaystyle \operatorname {apply} .}$

In der Mengenlehre bezeichnet man mit der Notation die Menge der Funktionen von der Menge A nach der Menge B. Currying ist die natürliche Bijektion zwischen der Menge der Funktionen von A nach B und der Menge der Funktionen von A nach B. In Symbolen: ${\displaystyle Y^{X}}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle A^{B\times C}}$${\displaystyle B\times C}$${\displaystyle A}$${\displaystyle (A^{C})^{B}}$${\displaystyle B}$${\displaystyle C}$${\displaystyle A}$

${\displaystyle A^{B\times C}\cong (A^{C})^{B}}$

Tatsächlich ist es diese natürliche Bijektion, die die Exponentialschreibweise für die Menge der Funktionen rechtfertigt. Wie in allen Fällen des Currying beschreibt die obige Formel ein adjungiertes Funktorenpaar : Für jede feste Menge ist der Funktor linksadjungiert zum Funktor . ${\displaystyle C}$${\displaystyle B\mapsto B\times C}$${\displaystyle A\mapsto A^{C}}$

In der Kategorie der Mengen wird das Objekt als Exponentialobjekt bezeichnet . ${\displaystyle Y^{X}}$

In der Theorie der Funktionenräume , etwa in der Funktionalanalysis oder der Homotopietheorie , interessiert man sich üblicherweise für stetige Funktionen zwischen topologischen Räumen . Man schreibt (den Hom-Funktor ) für die Menge aller Funktionen von nach und verwendet die Notation für die Teilmenge der stetigen Funktionen. Hierbei ist die Bijektion.${\displaystyle {\text{Hom}}(X,Y)}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle Y^{X}}$${\displaystyle {\text{curry}}}$

${\displaystyle {\text{curry}}:{\text{Hom}}(X\times Y,Z)\to {\text{Hom}}(X,{\text{Hom}}(Y,Z)),}$

Das Entcurrying ist die Umkehrabbildung. Wenn die Menge der stetigen Funktionen von nach durch die kompakt-offene Topologie gegeben ist und der Raum lokal kompakt Hausdorffsch ist , dann ${\displaystyle Y^{X}}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle Y}$

${\displaystyle {\text{curry}}:Z^{X\times Y}\to (Z^{Y})^{X}}$

ist ein Homöomorphismus . Dies ist auch der Fall, wenn , und kompakt erzeugt sind , ^{[ 17 ] : Kapitel 5 [ 18 ],} obwohl es noch weitere Fälle gibt. ^{[ 19 ] [ 20 ]}${\displaystyle X}$${\displaystyle Y}$${\displaystyle Y^{X}}$

Eine nützliche Folgerung ist, dass eine Funktion genau dann stetig ist, wenn ihre Curried-Form stetig ist. Ein weiteres wichtiges Ergebnis ist, dass die Anwendungsabbildung , in diesem Kontext üblicherweise als „Auswertung“ bezeichnet, stetig ist (beachten Sie, dass „eval“ in der Informatik ein völlig anderes Konzept ist). Das heißt:

${\displaystyle {\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}}$

ist stetig, wenn kompakt-offen und lokal kompakt Hausdorff ist. ^{[ 21 ]} Diese beiden Ergebnisse sind zentral für den Nachweis der Stetigkeit der Homotopie , d.h. wenn das Einheitsintervall ist , sodass man sich vorstellen kann, dass entweder eine Homotopie zweier Funktionen von nach ist oder, äquivalent dazu, ein einzelner (stetiger) Pfad in ist . ${\displaystyle Y^{X}}$${\displaystyle Y}$${\displaystyle X}$${\displaystyle I}$${\displaystyle Z^{I\times Y}\cong (Z^{Y})^{I}}$${\displaystyle Y}$${\displaystyle Z}$${\displaystyle Z^{Y}}$

In der algebraischen Topologie dient Currying als Beispiel für die Eckmann-Hilton-Dualität und spielt daher in verschiedenen Kontexten eine wichtige Rolle. Beispielsweise ist der Schleifenraum adjungiert zu reduzierten Suspensionen ; dies wird üblicherweise wie folgt geschrieben:

${\displaystyle [\Sigma X,Z]\approxeq [X,\Omega Z]}$

Dabei ist die Menge der Homotopieklassen von Abbildungen , die Suspension von A und der Schleifenraum von A. Im Wesentlichen kann die Suspension als kartesisches Produkt von mit dem Einheitsintervall modulo einer Äquivalenzrelation betrachtet werden, die das Intervall in eine Schleife umwandelt. Die Curry-Form bildet dann den Raum auf den Raum der Funktionen von Schleifen nach ab , d. h. von nach . ^{[ 21 ]} Dann ist der adjungierte Funktor , der Suspensionen auf Schleifenräume abbildet, und die Entcurryung ist der Duale. ^{[ 21 ]}${\displaystyle [A,B]}$${\displaystyle A\rightarrow B}$${\displaystyle \Sigma A}$${\displaystyle \Omega A}$${\displaystyle \Sigma X}$${\displaystyle X}$${\displaystyle X}$${\displaystyle Z}$${\displaystyle X}$${\displaystyle \Omega Z}$${\displaystyle {\text{curry}}}$

Die Dualität zwischen dem Abbildungskegel und der Abbildungsfaser ( Kofibration und Fibration ) ^{[ 17 ] : Kapitel 6,7} kann als eine Form des Currying verstanden werden, was wiederum zur Dualität der langen exakten und koexakten Puppe-Sequenzen führt .

In der homologischen Algebra wird die Beziehung zwischen Currying und Uncurrying als Tensor-Hom-Adjunktion bezeichnet . Hierbei ergibt sich eine interessante Besonderheit: Der Hom-Funktor und der Tensorproduktfunktor lassen sich möglicherweise nicht zu einer exakten Sequenz liften ; dies führt zur Definition des Ext-Funktors und des Tor-Funktors .

In der Ordnungstheorie , der Theorie der Verbände partiell geordneter Mengen , ist eine Funktion stetig, wenn dem Verband die Scott-Topologie gegeben ist . ^{[ 22 ]} Scott-stetige Funktionen wurden erstmals im Rahmen des Versuchs untersucht, eine Semantik für den Lambda-Kalkül zu entwickeln (da die gewöhnliche Mengenlehre hierfür nicht ausreicht). Allgemeiner werden Scott-stetige Funktionen heute in der Domänentheorie untersucht , die die denotationale Semantik von Computeralgorithmen umfasst. Die Scott-Topologie unterscheidet sich deutlich von vielen gängigen Topologien in der Kategorie der topologischen Räume ; sie ist typischerweise feiner und nicht nüchtern . ${\displaystyle {\text{curry}}}$

The notion of continuity makes its appearance in homotopy type theory, where, roughly speaking, two computer programs can be considered to be homotopic, i.e. compute the same results, if they can be "continuously" refactored from one to the other.

In theoretical computer science, currying provides a way to study functions with multiple arguments in very simple theoretical models, such as the lambda calculus, in which functions only take a single argument. Consider a function ${\displaystyle f(x,y)}$ taking two arguments, and having the type ${\displaystyle (X\times Y)\to Z}$, which should be understood to mean that x must have the type ${\displaystyle X}$, y must have the type ${\displaystyle Y}$, and the function itself returns the type ${\displaystyle Z}$. The curried form of f is defined as

${\displaystyle {\text{curry}}(f)=\lambda x.(\lambda y.(f(x,y)))}$

where ${\displaystyle \lambda }$ is the abstractor of lambda calculus. Since curry takes, as input, functions with the type ${\displaystyle (X\times Y)\to Z}$, one concludes that the type of curry itself is

${\displaystyle {\text{curry}}:((X\times Y)\to Z)\to (X\to (Y\to Z))}$

The → operator is often considered right-associative, so the curried function type ${\displaystyle X\to (Y\to Z)}$ is often written as ${\displaystyle X\to Y\to Z}$. Conversely, function application is considered to be left-associative, so that ${\displaystyle f(x,y)}$ is equivalent to

${\displaystyle (({\text{curry}}(f)\;x)\;y)={\text{curry}}(f)\;x\;y}$.

That is, the parenthesis are not required to disambiguate the order of the application.

Curried functions may be used in any programming language that supports closures; however, uncurried functions are generally preferred for efficiency reasons, since the overhead of partial application and closure creation can then be avoided for most function calls.

In type theory, the general idea of a type system in computer science is formalized into a specific algebra of types. For example, when writing ${\displaystyle f\colon X\to Y}$, the intent is that ${\displaystyle X}$ and ${\displaystyle Y}$ are types, while the arrow ${\displaystyle \to }$ is a type constructor, specifically, the function type or arrow type. Similarly, the Cartesian product ${\displaystyle X\times Y}$ of types is constructed by the product type constructor ${\displaystyle \times }$.

The type-theoretical approach is expressed in programming languages such as ML and the languages derived from and inspired by it: Caml, Haskell, and F#.

Der typentheoretische Ansatz ergänzt die Sprache der Kategorientheorie auf natürliche Weise , wie weiter unten erläutert wird. Kategorien, insbesondere monoidale Kategorien , besitzen eine interne Sprache , deren prominentestes Beispiel der einfach getypte Lambda-Kalkül ist. Dies ist in diesem Zusammenhang wichtig, da sie sich aus einem einzigen Typkonstruktor, dem Pfeiltyp, aufbauen lässt. Durch Currying erhält die Sprache dann einen natürlichen Produkttyp. Die Korrespondenz zwischen Objekten in Kategorien und Typen ermöglicht es, Programmiersprachen als Logiken (mittels Curry-Howard-Korrespondenz ) und als andere Arten mathematischer Systeme zu interpretieren , wie weiter unten erläutert wird.

Gemäß der Curry-Howard-Korrespondenz ist die Existenz von Currying und Uncurrying äquivalent zum logischen Theorem (auch bekannt als Exportation ), da Tupel ( Produkttyp ) der Konjunktion in der Logik entsprechen und der Funktionstyp der Implikation entspricht. ${\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}$

Das Exponentialobjekt in der Kategorie der Heyting-Algebren wird üblicherweise als materielle Implikation geschrieben . Distributive Heyting-Algebren sind Boolesche Algebren , und das Exponentialobjekt hat die explizite Form , wodurch deutlich wird, dass das Exponentialobjekt tatsächlich eine materielle Implikation ist . ^{[ 23 ]}${\displaystyle Q^{P}}$${\displaystyle P\to Q}$${\displaystyle \neg P\lor Q}$

Die oben genannten Begriffe des Currying und Uncurrying finden ihre allgemeinste, abstrakteste Formulierung in der Kategorientheorie . Currying ist eine universelle Eigenschaft eines Exponentialobjekts und führt zu einer Adjunktion in kartesisch abgeschlossenen Kategorien . Das heißt, es existiert ein natürlicher Isomorphismus zwischen den Morphismen von einem binären Produkt und den Morphismen zu einem Exponentialobjekt . ${\displaystyle f\colon (X\times Y)\to Z}$${\displaystyle g\colon X\to Z^{Y}}$

Dies lässt sich zu einem allgemeineren Ergebnis in geschlossenen monoidalen Kategorien verallgemeinern : Currying ist die Aussage, dass das Tensorprodukt und der interne Hom adjungierte Funktoren sind ; das heißt, zu jedem Objekt gibt es einen natürlichen Isomorphismus : ${\displaystyle B}$

${\displaystyle \mathrm {Hom} (A\otimes B,C)\cong \mathrm {Hom} (A,B\Rightarrow C).}$

Hier bezeichnet Hom den (externen) Hom-Funktor aller Morphismen in der Kategorie, während den internen Hom-Funktor in der abgeschlossenen monoidalen Kategorie bezeichnet. In der Kategorie der Mengen sind beide identisch. Ist das Produkt das kartesische Produkt, so entspricht der interne Hom-Funktor dem Exponentialobjekt . ${\displaystyle B\Rightarrow C}$${\displaystyle B\Rightarrow C}$${\displaystyle C^{B}}$

Currying kann auf zwei Arten fehlschlagen. Zum einen, wenn eine Kategorie nicht abgeschlossen ist und daher keinen internen Hom-Funktor besitzt (möglicherweise, weil es mehrere Möglichkeiten für einen solchen Funktor gibt). Zum anderen, wenn sie nicht monoidal ist und daher kein Produkt besitzt (d. h. keine Möglichkeit, Paare von Objekten darzustellen). Kategorien, die sowohl Produkte als auch interne Hom-Funktoren besitzen, sind genau die abgeschlossenen monoidalen Kategorien.

Die Betrachtung kartesisch abgeschlossener Kategorien genügt für die Diskussion der klassischen Logik ; die allgemeinere Betrachtung abgeschlossener monoidaler Kategorien eignet sich für die Quantenberechnung . ^{[ 24 ]}

Der Unterschied zwischen diesen beiden besteht darin, dass das Produkt für kartesische Kategorien (wie die Kategorie der Mengen , vollständige partielle Ordnungen oder Heyting-Algebren ) einfach das kartesische Produkt ist ; es wird als geordnetes Paar von Elementen (oder als Liste) interpretiert. Der einfach getypte Lambda-Kalkül ist die interne Sprache kartesisch abgeschlossener Kategorien; und aus diesem Grund sind Paare und Listen die primären Typen in der Typentheorie von LISP , Scheme und vielen funktionalen Programmiersprachen .

Im Gegensatz dazu ist das Produkt für monoidale Kategorien (wie Hilberträume und Vektorräume der Funktionalanalysis ) das Tensorprodukt . Die interne Sprache solcher Kategorien ist die lineare Logik , eine Form der Quantenlogik ; das zugehörige Typsystem ist das lineare Typsystem . Solche Kategorien eignen sich zur Beschreibung verschränkter Quantenzustände und ermöglichen allgemein eine umfassende Verallgemeinerung der Curry-Howard-Korrespondenz auf die Quantenmechanik , auf Kobordismen in der algebraischen Topologie und auf die Stringtheorie . ^{[ 3 ]} Das lineare Typsystem und die lineare Logik sind nützlich zur Beschreibung von Synchronisationsprimitiven , wie z. B. wechselseitigen Ausschlussmechanismen und der Funktionsweise von Verkaufsautomaten.

Currying und partielle Funktionsanwendung werden oft verwechselt. ^{[ 1 ] [ 2 ]} Ein wesentlicher Unterschied zwischen den beiden besteht darin, dass ein Aufruf einer partiell angewendeten Funktion das Ergebnis sofort zurückgibt und nicht eine weitere Funktion in der Currying-Kette; dieser Unterschied lässt sich besonders gut bei Funktionen mit mehr als zwei Stelligkeiten veranschaulichen. ^{[ 25 ]}

Bei einer Funktion vom Typ `f` erzeugt Currying das Ergebnis `f` . Das heißt, während die Auswertung der ersten Funktion als `f` dargestellt werden könnte , würde die Auswertung der gecurryten Funktion als `f` dargestellt , wobei jedes Argument nacheinander auf eine Funktion mit einem Argument angewendet wird, die vom vorherigen Aufruf zurückgegeben wurde. Beachten Sie, dass wir nach dem Aufruf von `f` eine Funktion erhalten, die ein einzelnes Argument entgegennimmt und eine andere Funktion zurückgibt, nicht eine Funktion, die zwei Argumente entgegennimmt. ${\displaystyle f\colon (X\times Y\times Z)\to N}$${\displaystyle {\text{curry}}(f)\colon X\to (Y\to (Z\to N))}$${\displaystyle f(1,2,3)}$${\displaystyle f_{\text{curried}}(1)(2)(3)}$${\displaystyle f_{\text{curried}}(1)}$

Im Gegensatz dazu bezeichnet die partielle Funktionsanwendung das Festlegen einer bestimmten Anzahl von Argumenten einer Funktion, wodurch eine Funktion mit geringerer Stelligkeit entsteht. Gemäß der obigen Definition könnten wir das erste Argument festlegen (oder „binden“) und so eine Funktion vom Typ erhalten . Die Auswertung dieser Funktion ließe sich wie folgt darstellen : . Beachten Sie, dass das Ergebnis der partiellen Funktionsanwendung in diesem Fall eine Funktion mit zwei Argumenten ist. ${\displaystyle f}$${\displaystyle {\text{partial}}(f)\colon (Y\times Z)\to N}$${\displaystyle f_{\text{partial}}(2,3)}$

Intuitiv bedeutet partielle Funktionsanwendung: „Wenn man das erste Argument der Funktion festlegt, erhält man eine Funktion der verbleibenden Argumente.“ Wenn beispielsweise die Funktion div für die Division x / y steht , dann ist div mit dem Parameter x auf 1 festgelegt (d. h. div 1) eine andere Funktion: dieselbe wie die Funktion inv , die das multiplikative Inverse ihres Arguments zurückgibt, definiert durch inv ( y ) = 1/ y .

Die praktische Motivation für die partielle Anwendung liegt darin, dass die Funktionen, die durch Übergabe einiger, aber nicht aller Argumente einer Funktion entstehen, oft nützlich sind; beispielsweise verfügen viele Programmiersprachen über eine Funktion oder einen Operator, der dem Additionsoperator ähnelt plus_one. Die partielle Anwendung vereinfacht die Definition solcher Funktionen, etwa durch die Erstellung einer Funktion, die den Additionsoperator mit der Grenze 1 als erstem Argument repräsentiert.

Eine partielle Anwendung kann als Auswertung einer curried Funktion an einem Fixpunkt betrachtet werden, z. B. gegeben und dann oder einfach wo der erste Parameter von f curried wird. ${\displaystyle f\colon (X\times Y\times Z)\to N}$${\displaystyle a\in X}$${\displaystyle {\text{curry}}({\text{partial}}(f)_{a})(y)(z)={\text{curry}}(f)(a)(y)(z)}$${\displaystyle {\text{partial}}(f)_{a}={\text{curry}}_{1}(f)(a)}$${\displaystyle {\text{curry}}_{1}}$

Somit reduziert sich die partielle Anwendung auf eine Curry-Funktion an einem Fixpunkt. Weiterhin ist eine Curry-Funktion an einem Fixpunkt (trivialerweise) eine partielle Anwendung. Ein weiterer Beweis dafür ist, dass zu jeder Funktion eine Funktion definiert werden kann, sodass . Somit lässt sich jede partielle Anwendung auf eine einzelne Curry-Operation reduzieren. Daher ist Curry treffender als eine Operation zu definieren, die in vielen theoretischen Fällen rekursiv angewendet wird, aber theoretisch (als Operation betrachtet) nicht von einer partiellen Anwendung zu unterscheiden ist. ${\displaystyle f(x,y)}$${\displaystyle g(y,x)}$${\displaystyle g(y,x)=f(x,y)}$

Eine partielle Anwendung kann also als das objektive Ergebnis einer einzelnen Anwendung des Curry-Operators auf eine bestimmte Reihenfolge der Eingaben einer Funktion definiert werden.

• Tensor-Hom-Adjunktion
• Faule Bewertung
• Abschluss (Computerprogrammierung)
• S m n Satz
• Geschlossene monoidale Kategorie