curry

En théorie des ensembles , la notation

En effet, c'est cette bijection naturelle qui justifie la notation exponentielle pour l'ensemble des fonctions. Comme c'est le cas dans tous les cas de curryfication, la formule ci-dessus décrit une paire de foncteurs adjoints : pour tout ensemble fixé

Dans la catégorie des ensembles , l' objet

Dans la théorie des espaces fonctionnels , comme en analyse fonctionnelle ou en théorie de l'homotopie , on s'intéresse généralement aux fonctions continues entre espaces topologiques . On écrit :toutes les fonctions de

tandis que le décurryage est l'application inverse. Si l'ensemble

est un homéomorphisme . C'est également le cas lorsque

Un corollaire utile est qu'une fonction est continue si et seulement si sa forme curryfiée est continue. Un autre résultat important est que l' application , généralement appelée « évaluation » dans ce contexte, est continue (notez que le terme « évaluation » est un concept strictement différent en informatique). Autrement dit,

est continu lorsque

En topologie algébrique , la curryfication est un exemple de dualité d'Eckmann-Hilton et, à ce titre, joue un rôle important dans divers contextes. Par exemple, l'espace des lacets est adjoint aux suspensions réduites ; on écrit généralement ceci comme

oùA , etA. En substance, la suspension

La dualité entre le cône de cartographie et la fibre de cartographie ( cofibration et fibration ) peut être comprise comme une forme de curryfication, qui à son tour conduit à la dualité des longues séquences Puppe exactes et coexactes .

En algèbre homologique , la relation entre curryfication et décurryfication est appelée adjonction tenseur-hom . Un phénomène intéressant apparaît alors : le foncteur Hom et le foncteur produit tensoriel ne se relèvent pas nécessairement en une suite exacte ; ceci conduit à la définition des foncteurs Ext et Tor .

En théorie de l'ordre , la théorie des treillis d' ensembles partiellement ordonnés ,

La notion de continuité apparaît dans la théorie des types homotopiques , où, en gros, deux programmes informatiques peuvent être considérés comme homotopiques, c'est-à-dire qu'ils calculent les mêmes résultats, s'ils peuvent être refactorisés «continuellement» de l'un à l'autre.

En informatique théorique , la curryfication permet d'étudier les fonctions à plusieurs arguments dans des modèles théoriques très simples, comme le lambda-calcul , où les fonctions ne prennent qu'un seul argument. Prenons l'exemple d'une fonctionx doit avoir le typey doit avoir le typef est définie comme

où

L'opérateur → est souvent considéré comme associatif à droite , donc le type de fonction curryfiée

Autrement dit, les parenthèses ne sont pas nécessaires pour lever toute ambiguïté quant à l'ordre de l'application.

Les fonctions curryfiées peuvent être utilisées dans tout langage de programmation prenant en charge les fermetures ; cependant, les fonctions non curryfiées sont généralement préférées pour des raisons d’efficacité, car la surcharge liée à l’application partielle et à la création de fermetures peut alors être évitée pour la plupart des appels de fonction.

En théorie des types , l'idée générale d'un système de types en informatique est formalisée en une algèbre de types spécifique. Par exemple, lors de l'écriture

L'approche théorique des types est exprimée dans des langages de programmation tels que ML et les langages qui en sont dérivés et qui s'en inspirent : Caml , Haskell et F# .

L'approche typée complète naturellement le langage de la théorie des catégories , comme nous le verrons plus loin. En effet, les catégories, et plus particulièrement les catégories monoïdales , possèdent un langage interne , dont le lambda-calcul simplement typé est l'exemple le plus emblématique. Ce langage est important ici car il peut être construit à partir d'un unique constructeur de type : le type flèche. La curryfication dote alors ce langage d'un type produit naturel. La correspondance entre les objets des catégories et les types permet ainsi de réinterpréter les langages de programmation comme des logiques (via la correspondance de Curry-Howard ) et comme d'autres types de systèmes mathématiques, comme nous le verrons plus loin.

Dans le cadre de la correspondance de Curry-Howard , l'existence du currying et du décurrying est équivalente au théorème logique

L' objet exponentiel

Les notions de curryfication et de décurryfication mentionnées ci-dessus trouvent leur formulation la plus générale et abstraite en théorie des catégories . La curryfication est une propriété universelle d'un objet exponentiel et induit une adjonction dans les catégories cartésiennes fermées . Autrement dit, il existe un isomorphisme naturel entre les morphismes d'un produit binaire.

Ce résultat se généralise à un résultat plus large dans les catégories monoïdales fermées : la curryfication est l’affirmation que le produit tensoriel et le Hom interne sont des foncteurs adjoints ; c’est-à-dire que pour tout objet

Ici, Hom désigne le foncteur Hom (externe) de tous les morphismes de la catégorie, tandis que

La curryfication peut échouer de deux manières. Premièrement, si une catégorie n'est pas fermée et ne possède donc pas de foncteur hom interne (il est possible qu'il existe plusieurs choix pour un tel foncteur). Deuxièmement, si elle n'est pas monoïdale et ne possède donc pas de produit (c'est-à-dire qu'elle ne permet pas de représenter des paires d'objets). Les catégories qui possèdent à la fois un produit et un foncteur hom interne sont précisément les catégories monoïdales fermées.

Le cadre des catégories fermées cartésiennes est suffisant pour la discussion de la logique classique ; le cadre plus général des catégories monoïdales fermées convient au calcul quantique .

La différence entre ces deux notions réside dans le fait que le produit des catégories cartésiennes (telles que la catégorie des ensembles , les ordres partiels complets ou les algèbres de Heyting ) est simplement le produit cartésien ; il est interprété comme une paire ordonnée d’éléments (ou une liste). Le lambda-calcul, simplement typé, est le langage interne des catégories cartésiennes fermées ; c’est pourquoi les paires et les listes sont les types primaires de la théorie des types de LISP , Scheme et de nombreux langages de programmation fonctionnelle .

En revanche, le produit des catégories monoïdales (telles que l'espace de Hilbert et les espaces vectoriels de l'analyse fonctionnelle ) est le produit tensoriel . Le langage interne de ces catégories est la logique linéaire , une forme de logique quantique ; le système de types correspondant est le système de types linéaires . Ces catégories conviennent à la description d'états quantiques intriqués et, plus généralement, permettent une vaste généralisation de la correspondance de Curry-Howard à la mécanique quantique , aux cobordismes en topologie algébrique et à la théorie des cordes . Le système de types linéaires et la logique linéaire sont utiles pour décrire les primitives de synchronisation , telles que les verrous d'exclusion mutuelle, et le fonctionnement des distributeurs automatiques.