У математици и рачунарству, каринг (енгл. currying) јесте техника трансформације функције која прима више аргумената у низ породица функција, од којих свака прима по један аргумент.
У прототипском примеру, почиње се са функцијом која узима два аргумента, један из и један из и производи објекте у Каринг облик ове функције третира први аргумент као параметар, како би се створила породица функција Породица је уређена тако да за сваки објекат у постоји тачно једна функција , таква да за свако у , важи .
У овом примеру, и само постаје функција која узима као аргумент и враћа функцију која пресликава свако у Правилна нотација за изражавање овога је опширна. Функција припада скупу функција У међувремену, припада скупу функција Дакле, нешто што пресликава у биће типа Са овом нотацијом, је функција која узима објекте из првог скупа и враћа објекте у другом скупу, па се пише Ово је помало неформалан пример; прецизније дефиниције онога што се подразумева под „објектом” и „функцијом” дате су у наставку. Ове дефиниције варирају од контекста до контекста и узимају различите облике, у зависности од теорије у којој се ради.
Каринг је повезан са, али није исто што и делимична примена функције. Пример изнад може се користити за илустрацију делимичне примене; прилично је сличан. Делимична примена је функција која узима пар и заједно као аргументе и враћа Користећи исту нотацију као горе, делимична примена има потпис Написано на овај начин, примена се може видети као адјунгована карингу.
Каринг функције са више од два аргумента може се дефинисати индукцијом.
Каринг је користан и у практичним и у теоријским поставкама. У функционалним програмским језицима, и многим другим, пружа начин за аутоматско управљање прослеђивањем аргумената функцијама и изузецима. У теоријском рачунарству, пружа начин за проучавање функција са више аргумената у једноставнијим теоријским моделима који пружају само један аргумент. Најопштија поставка за строги појам каринга и „отказивања” каринга (енгл. uncurrying) је у затвореним моноидалним категоријама, што чини основу за огромну генерализацију Кари—Хауард кореспонденције доказа и програма на кореспонденцију са многим другим структурама, укључујући квантну механику, кобордизме и теорију струна.
Концепт каринга увео је Готлоб Фреге, развио га је Мозес Шенфинкел,Првобитно објављено као
Поново објављено као а даље развио Хаскел Кари.
Опозвани каринг (енгл. Uncurrying) дуална је трансформација карингу и може се видети као облик дефункционализације. Узима функцију чија је повратна вредност друга функција , и даје нову функцију која као параметре узима аргументе и за и за , и враћа, као резултат, примену а затим на те аргументе. Процес се може итерирати.
Мотивација Каринг пружа начин за рад са функцијама које узимају више аргумената, и њихово коришћење у оквирима где функције могу узимати само један аргумент. На пример, неке аналитичке технике могу се применити само на функције са једним аргументом. Практичне функције често узимају више аргумената. Фреге је показао да је довољно обезбедити решења за случај са једним аргументом, јер је могуће трансформисати функцију са више аргумената у ланац функција са једним аргументом. Ова трансформација је процес данас познат као каринг. Све „обичне” функције које се типично срећу у математичкој анализи или у програмирању могу се каровати. Међутим, постоје категорије у којима каринг није могућ; најопштије категорије које дозвољавају каринг су затворене моноидалне категорије.
Неки програмски језици готово увек користе кароване функције за постизање вишеструких аргумената; значајни примери су ML и Хаскел, где у оба случаја све функције имају тачно један аргумент. Ово својство је наслеђено из ламбда рачуна, где су функције са више аргумената обично представљене у карованом облику.
Каринг је повезан са, али није исто што и делимична примена функције. У пракси, програмска техника затворења (енгл. closure) може се користити за извођење делимичне примене и врсте каринга, скривањем аргумената у окружењу које путује са карованом функцијом.
Историја Назив „Каринг” (енгл. Currying) референца је на логичара Хаскела Карија, који је интензивно користио овај концепт, али Мозес Шенфинкел је имао идеју шест година пре Карија. Алтернативни назив „Шенфинкелизација” је био предложен. У математичком контексту, принцип се може пратити до рада Фрегеа из 1893. године.
Творац речи „каринг” није јасан. Дејвид Тарнер каже да је реч сковао Кристофер Стрејчи у својим белешкама са предавања из 1967. године Fundamental Concepts in Programming Languages, али тај извор уводи концепт као „уређај који је осмислио Шенфинкел”, а термин „каринг” се не користи, док се Кари помиње касније у контексту функција вишег реда. Џон К. Рејнолдс је дефинисао „каринг” у раду из 1972. године, али није тврдио да је сковао термин.
Дефиниција Каринг се најлакше разуме почевши од неформалне дефиниције, која се затим може обликовати да одговара многим различитим доменима. Прво, потребно је успоставити неку нотацију. Нотација означава све функције од до . Ако је таква функција, пишемо . Нека означава уређене парове елемената из и респективно, то јест, Декартов производ и . Овде, и могу бити скупови, или могу бити типови, или могу бити друге врсте објеката, као што је истражено у наставку.
Дату функцију
,
каринг конструише нову функцију
.
То јест, узима аргумент типа и враћа функцију типа . Дефинисана је са
за типа и типа . Тада такође пишемо
Опозвани каринг (енгл. Uncurrying) је обрнута трансформација и најлакше се разуме у смислу њеног десног адјункта, функције
Теорија скупова У теорији скупова, нотација користи се за означавање скупа функција из скупа у скуп . Каринг је природна бијекција између скупа функција од до , и скупа функција од до скупа функција од до . Симболички:
Заиста, управо ова природна бијекција оправдава експоненцијалну нотацију за скуп функција. Као што је случај у свим инстанцама каринга, горња формула описује адјунговани пар функтора: за сваки фиксни скуп , функтор је леви адјункт функтора .
У категорији скупова, објекат назива се експоненцијални објекат.
Простор функција У теорији простора функција, као што је у функционалној анализи или теорији хомотопије, често се интересујемо за непрекидне функције између тополошких простора. Пише се (Hom функтор) за скуп свих функција од до , и користи се нотација за означавање подскупа непрекидних функција. Овде, је бијекција
док је опозвани каринг инверзно пресликавање. Ако је скупу непрекидних функција од до дата топологија компакт-отворено, и ако је простор локално компактан Хаусдорфов простор, тада је
хомеоморфизам. Ово је такође случај када су , и компактно генерисани, иако постоји више случајева.
Једна корисна последица је да је функција непрекидна ако и само ако је њен каровани облик непрекидан. Други важан резултат је да је мапа примене, обично названа „евалуација” у овом контексту, непрекидна (имајте на уму да је eval строго различит концепт у рачунарству). То јест,
је непрекидно када је компакт-отворено и локално компактан Хаусдорфов простор. Ова два резултата су централна за успостављање непрекидности хомотопије, тј. када је јединични интервал , тако да се може посматрати или као хомотопија две функције од до , или, еквивалентно, као једна (непрекидна) путања у .
Алгебарска топологија У алгебарској топологији, каринг служи као пример Екман-Хилтонове дуалности, и као такав игра важну улогу у различитим поставкама. На пример, простор петљи је адјунгован редукованим суспензијама; ово се обично пише као
где је скуп класа хомотопије мапа , а је суспензија од A, и је простор петљи од A. У суштини, суспензија се може видети као Декартов производ са јединичним интервалом, модуло релација еквиваленције која претвара интервал у петљу. Каровани облик затим пресликава простор у простор функција из петљи у , то јест, из у . Тада је адјунговани функтор који пресликава суспензије у просторе петљи, а опозвани каринг је дуал.
Дуалност између конуса пресликавања и влакна пресликавања (кофибрација и фибрација) може се разумети као облик каринга, што заузврат води до дуалности дугих егзактних и коегзактних Пупеових низова.
У хомолошкој алгебри, однос између каринга и опозваног каринга познат је као тензор-хом адјункција. Овде се јавља занимљив обрт: Хом функтор и функтор тензорски производ можда се неће подићи у егзактни низ; ово води до дефиниције Ext функтора и Tor функтора.
Теорија домена У теорији поретка, теорији мрежа парцијално уређених скупова, је непрекидна функција када је мрежи дата Скотова топологија. Скот-непрекидне функције су први пут истраживане у покушају да се обезбеди семантика за ламбда рачун (пошто обична теорија скупова није адекватна за то). Општије, Скот-непрекидне функције се сада проучавају у теорији домена, која обухвата проучавање денотационе семантике рачунарских алгоритама. Имајте на уму да је Скотова топологија прилично различита од многих уобичајених топологија које се могу срести у категорији тополошких простора; Скотова топологија је типично финија, и није трезвена.
Појам непрекидности се појављује у хомотопској теорији типова, где се, грубо говорећи, два рачунарска програма могу сматрати хомотопским, тј. израчунавају исте резултате, ако се могу „непрекидно” рефакторисати из једног у други.
Ламбда рачун У теоријском рачунарству, каринг пружа начин за проучавање функција са више аргумената у веома једноставним теоријским моделима, као што је ламбда рачун, у којем функције узимају само један аргумент. Размотримо функцију која узима два аргумента и има тип , што треба разумети тако да x мора имати тип , y мора имати тип , а сама функција враћа тип . Каровани облик од f дефинисан је као
где је апстрактор ламбда рачуна. Пошто кари узима, као улаз, функције типа , закључује се да је тип самог карија
Оператор → се често сматра десно асоцијативним, па се тип кароване функције често пише као . Обрнуто, примена функције се сматра лево асоцијативном, тако да је еквивалентно са
.
То јест, заграде нису потребне да би се разјаснио редослед примене.
Кароване функције се могу користити у било ком програмском језику који подржава затворења; међутим, некароване функције се генерално преферирају из разлога ефикасности, пошто се трошкови делимичне примене и креирања затворења тада могу избећи за већину позива функција.
Теорија типова У теорији типова, општа идеја система типова у рачунарству формализована је у специфичну алгебру типова. На пример, када пишемо , намера је да су и типови, док је стрелица конструктор типа, конкретно, функцијски тип или стрелица тип. Слично, Декартов производ типова конструисан је конструктором производа типа .
Приступ теорије типова изражен је у програмским језицима као што су ML и језици изведени из њега и инспирисани њиме: Caml, Хаскел и F#.
Приступ теорије типова пружа природну допуну језику теорије категорија, као што је дискутовано у наставку. То је зато што категорије, и конкретно, моноидалне категорије, имају интерни језик, при чему је једноставно типизирани ламбда рачун најистакнутији пример таквог језика. Важан је у овом контексту јер се може изградити из једног конструктора типа, стрелица типа. Каринг тада дарује језику природни производни тип. Кореспонденција између објеката у категоријама и типова тада омогућава да се програмски језици поново интерпретирају као логике (преко Кари—Хауард кореспонденције), и као друге врсте математичких система, као што је даље истражено у наставку.
Логика Под Кари—Хауард кореспонденцијом, постојање каринга и опозваног каринга еквивалентно је логичкој теореми (такође познато као извоз), јер торке (производни тип) одговарају конјункцији у логици, а функцијски тип одговара импликацији.
Експоненцијални објекат у категорији Хејтингових алгебри обично се пише као материјална импликација . Дистрибутивне Хејтингове алгебре су Булове алгебре, и експоненцијални објекат има експлицитни облик , чинећи јасним да је експоненцијални објекат заиста материјална импликација.
Теорија категорија