Catamorfisme și F-algebre

așa că aud adesea cuvintele” catamorfism “și”scheme de recursivitate”. Despre ce e vorba?

Catamorfismele (sau cata) sunt generalizări ale conceptului de pliu în programarea funcțională. Având în vedere o f-algebră și o structură de date recursivă, un catamorfism va produce o valoare evaluând recursiv structura dvs. de date.

ce este o algebră F? Poate puteți arăta mai întâi câteva exemple de cod?

configurarea nu este atât de simplă, așa că să începem simplu. Să presupunem că aveți următoarea structură de date pentru a reprezenta o expresie:

și o expresie simplă poate arăta astfel:

având doar o structură de date expresie este inutil, desigur, veți avea nevoie de o funcție pentru a evalua și a obține rezultatul:

aici vine generalizarea catamorfismului:

🤨, dar ce rost are? Doar aplici un argument unei funcții?

asta pentru că este notReallyCata. Funcția real cata este generică și nu depinde de o anumită structură de date sau funcție de evaluator. A se vedea, crearea unei structuri de date recursive și apoi pliere peste ea este un model comun care cata încearcă să generalizeze.

Ok, atunci cum arată adevărata cata?

🤯

de aceea am început cu notReallyCata. Vom descompune implementarea mai târziu până când face clic. Dar acum să continuăm cu exemplul nostru Expression. În primul rând, trebuie să scăpăm de recursivitate prin introducerea unui parametru de tip:

toate referințele la Expression sunt înlocuite cu a parametru de tip astfel încât structura de date nu mai este recursivă.

de ce există un F la sfârșitul constructorilor de tip?

Mă bucur că ai întrebat — Asta e un indiciu că ExpressionF poate fi un Functor:

nimic fantezie, doar aplicarea unor funcții la valoarea învelite păstrarea stucture.

nu sunt sigur de ce avem nevoie de asta 🤔

nu are sens acum, dar va fi un pic mai târziu. Acum, modul în care ne creăm expresia nu s-a schimbat (cu excepția numelor constructorilor):

dar tipul rezultat este diferit:

expr prăbușește totul într-un singur Expression în timp ce exprF codifică informații despre nivelul de cuibărit al arborelui nostru de Expresie. Vorbind despre evaluare, acesta este modul în care putem merge despre implementarea eval pentru ExpressionF:

principala diferență cu originalul evalExpr este că nu avem apel recursiv la evalExprF(ExpressionF nu este recursiv, îți amintești?). De asemenea, înseamnă că evaluatorul nostru poate lucra numai cu o expresie de un singur nivel:

și nu va compila pe această:

pur și simplu pentru că exprF expepects ExpressionF Int și ne împinge ExpressionF (ExpressionF Int).

pentru a face să funcționeze am putea defini un alt evaluator:

se pare cam ad-hoc, ce se întâmplă dacă aveți expresii profund imbricate?

Da, pentru expresia imbricată arbitrară această abordare nu este scalabilă — fiecare nivel suplimentar de cuibărire necesită scrierea funcției specializate.

există o modalitate de a generaliza acest cuib cu un nou tip:

să repar? Pare o structură de date recursivă care nu face mare lucru. Cum este util?

să ne uităm mai întâi la Expresie înainte de semnul egal: într-adevăr Fixeste o structură de date recursivă care are un parametru de tip f. Acest parametru are un fel * -> * de exemplu, este nevoie, de asemenea, un parametru de tip. De exemplu, nu puteți construi Fix oferind Int sau Bool, trebuie să fie ceva de genul Maybe, List sau… ExpressionF. Acesta este motivul pentru care am introdus parametrul de tip pentru ExpressionF. Apoi, după semnul egal avem un singur constructor de tip Fx luând un singur argument de tip f (Fix f) care este practic o expresie care construiește valoarea f. În cazul Maybe ar fi Maybe (Fix Maybe) și apoi totul este înfășurat cu Fxîn tipul Fix Maybe.

semnătura de tip este confuz pentru a citi la început din cauza constructorului de tip poate avea același nume ca și tipul în sine, plus auto referențiere. Dar nu este mult mai mult decât doar înfășurarea unui tip de ordin superior într-o structură de date. Btw, unfix este un opus Fx și tot ce face este model de potrivire pe Fx și returnează valoarea înfășurat, nu e mare lucru.

acum, vom înlocui fiecare ExpressionF din arborele nostru de Expresie cu Fix ExpressionF. Observați diferența în construirea expresiilor cu și fără Fx — sunt practic aceleași, cu excepția faptului că trebuie să ne prefacem Fx $:

tipul rezultat al unei versiuni ‘fixe’ este Fix ExpressionF deci ne-am întors la o reprezentare recursivă, dar acum trebuie să folosim funcția unfix pentru a obține structura noastră de date nerecursivă înapoi.

care sunt beneficiile de a avea Fix? Se pare că este aceeași abordare ca și tipul original Expression, dar acum avem acest ciudat Fix și unfix prostii?

Da, dar încercăm să generalizăm procesul de pliere, necesită introducerea unor abstracții suplimentare, cum ar fi Fix și Algebra pe care le vom discuta mai târziu. Poartă-te cu mine, ar trebui să aibă mai mult sens mai târziu.

deci avem structura noastră de date ‘fixă’, cum ar arăta funcția de evaluare?

având în vedere un Fix ExpressionF singurul lucru pe care îl putem face cu ea este de asteptare unfix care produce ExpressionF (Fix ExpressionF):

returnatul ExpressionF poate fi unul dintre ValueF, AddF sau MultF având un Fix ExpressionF ca parametru de tip. Este logic să faceți potrivirea modelelor și să decideți ce să faceți în continuare:

Da, arată la fel ca primul nostru evaluator recursiv pentru Expression cu adăugarea de a fi nevoie să desfaceți expresia cu unfix. Deci, de ce deranjez cu Fix oricum?

iată cheia: vom reutiliza evaluatorul original ‘fix-less’ pentru ExpressionF și îl vom distribui cumva pe structura Fix ExpressionF. Deci, aceasta ar trebui să fie o funcție care să ia două argumente-evaluatorul și structura de evaluat:

să încercăm să ne dăm seama de implementare — primul lucru logic de făcut este să folosiți unfix pentru a obține ExpressionF și apoi poate să-l transmiteți evaluator:

evident, acest lucru nu funcționează, evaluator se așteaptă ExpressionF Int și nu ExpressionF (Fix ExpressionF). Apropo, amintiți-vă că ExpressionF este un Functor? Aici devine util — putem folosi fmap pentru a aplica același proces la nivelul interior al arborelui nostru de Expresie:

luați un moment și gândiți-vă la ce se întâmplă: trecem o funcție recursivă almostCata evaluator în fmap. Dacă expresia curentă este AddF sau MultF atunci această funcție va fi trecută cu un nivel mai adânc și fmap va fi apelată din nou. Acest lucru se va întâmpla până când vom ajunge la ValueF, fmapping peste ValueF returnează valoarea de tip ExpressionF Int și asta e exact ceea ce acceptă funcția noastră evaluator.

uitându-ne la almostCata putem vedea că nu are nimic specific tipului ExpressionF sau Int și teoretic poate fi generalizat cu un parametru de tip f. Singura constrângere ar trebui să aibă o instanță Functor pentru f , deoarece folosim fmap:

și aceasta este versiunea finală a cata. Iată implementarea completă cu câteva exemple de utilizare:

cred că e în regulă. Dar de ce tho?

o mulțime de concepte în teoria categoriilor și programarea funcțională sunt destul de abstracte și uneori este greu să găsești aplicații practice imediate pentru anumite idei. Dar căutarea abstracțiilor și generalizărilor este utilă pentru a găsi modele și soluții elegante la probleme care altfel necesită implementare ad-hoc.

apropo, generalizând funcția noastră ExpressionF -> Int la Functor f => (f a -> a) am descoperit un alt concept important numit F-Algebra. Practic F-Algebra este un triplu de functor f, unele tip ași funcția de evaluator f a -> a. Rețineți că a aici nu polimorf — trebuie să fie un tip concret, cum ar fi Int sau Bool și se numește tip purtător. Pentru orice endo-functor f puteți crea mai multe F-Algebra bazat pe ea. Luați exemplul nostru de expresii-endo-functor f este ExpressionF, a este Intși evaluator este evalExprF. Dar putem schimba tipul de purtător și să producem mai multe algebre:

sunt doar evaluatori diferiți care pot fi trecuți în cata, nu?

Da, alegem diferite tipuri de transportatori și alegem implementarea noastră. Dar există truc — există o mamă a tuturor evaluatorilor pe care le putem crea prin alegerea tipului nostru de transport să fie… Fix ExprF.

evaluarea la Int sau Bool are sens, dar ce ar evalua acest initialAlgebra? Când trebuie să am Fix de ceva ca rezultat al evaluatorului meu?

desigur, nu veți scrie singur așa ceva, vreau doar să vă arăt sensul mai profund din spatele F-algebrelor și cata. De fapt, avem deja o implementare pentru astfel de evaluator și asta e exact Fx constructor:

stai, Fx este un evaluator? E o nebunie.

Da și face cel mai simplu lucru pe care îl puteți face — salvați expession într-o structură de date. În timp ce toți ceilalți evaluatori (algebra0, algebra1) au produs o anumită valoare prin reducerea expresiei (cum ar fi suma sau concatenarea) Fx doar înfășoară expresia fără a pierde date.

acesta este motivul pentru care am introdus Fix în primul rând — evaluați mai întâi structura de date originală cu Fx în algebra inițială Fix f și apoi folosind cataevaluarea ‘reală’ se întâmplă prin fmap ing evaluatorul dvs. concret peste algebra initală.

din punct de vedere al teoriei categoriilor, toate algebrele bazate pe același endo-functor formează o categorie. Această categorie are un obiect inițial care este algebra noastră inițială creată prin alegerea tipului de purtător ca Fix f. Există câteva postări grozave pe blog ale lui Bartosz Milewski pe care vă recomand să le verificați dacă doriți să obțineți o înțelegere categorică profundă.

este încă destul de greu de înțeles, nu cred că înțeleg pe deplin conceptul

este întotdeauna mai bine să faceți mâinile pe: încercați să re-implementați Fix și cata pe cont propriu, gândiți-vă la posibile structuri de date și algebre. De exemplu, un String poate fi reprezentat recursiv (ca Char cap și coadă de String), length al unui șir poate fi calculat cu cata. Iată câteva resurse excelente pentru citirea ulterioară:

• înțelegerea F-algebrelor și A F-algebrelor ușor diferite de Bartosz Milewski
• Catamorfisme în 15 minute de Chris Jones
• programare de baze de date funcționale Pure cu tipuri de puncte fixe de Rob Norris
• Catamorfisme pe Haskell wiki
• scheme practice de recursivitate de Jared Tobin