Katamorfier og F-algebraer

så jeg hører ofte ordene” katamorfisme “og”rekursionsordninger”. Hvad handler det om?

Katamorfier (eller cata) er generaliseringer af begrebet en fold i funktionel programmering. Givet en F-Algebra og en rekursiv datastruktur vil en katamorfisme producere en værdi ved rekursivt at evaluere din datastruktur.

Hvad er en F-Algebra? Måske kan du først vise nogle kodeeksempler?

opsætningen er ikke så ligetil, så lad os starte simpelt. Lad os sige, at du har følgende datastruktur til at repræsentere et udtryk:

og et simpelt udtryk kan se sådan ud:

at have bare et udtryk datastruktur er ubrugelig, selvfølgelig skal du bruge en funktion til at evaluere og få resultatet:

det er her, hvor generalisering af katamorfisme kommer ind:

🤨, men hvad er pointen? Du bare anvende et argument til en funktion?

det er fordi det er notReallyCata. Den virkelige cata funktion er generisk og afhænger ikke af nogen bestemt datastruktur eller evaluatorfunktion. Se, Oprettelse af en rekursiv datastruktur og derefter foldning over den er et almindeligt mønster, som cata forsøger at generalisere.

Ok, så hvordan ser den rigtige cata ud?

🤯

derfor startede vi med notReallyCata. Vi nedbryder implementeringen senere, indtil den klikker. Men lad os nu fortsætte med vores Expression eksempel. For det første skal vi slippe af med rekursion ved at indføre en typeparameter:

alle henvisninger til Expression erstattes med a typeparameter, så datastrukturen ikke længere er rekursiv.

Hvorfor er der en F i slutningen af typen konstruktører?

Glad for du spurgte-det er et tip, at ExpressionF kan være en Functor:

intet fancy, bare anvende nogle funktion til den indpakkede værdi bevare struktur.

ikke sikker på, hvorfor vi har brug for det 🤔

det giver ikke mening nu, men det vil lidt senere. Nu er den måde, vi skaber vores udtryk på, ikke ændret (undtagen konstruktørnavne):

men den resulterende type er anderledes:

expr kollapser alt i en enkelt Expression mens exprF koder for information om nesteniveauet for vores udtrykstræ. Når vi taler om evaluering, er det sådan, Vi kan gå i gang med at implementere eval for ExpressionF:

den største forskel med original evalExpr er, at vi ikke har rekursivt opkald til evalExprF (ExpressionF er ikke rekursiv, husk?). Det betyder også, at vores evaluator kun kan arbejde med et enkelt niveau udtryk:

og vil ikke kompilere på dette:

simpelthen fordi exprF forventer ExpressionF Intog vi skubber ExpressionF (ExpressionF Int).

for at få det til at fungere kunne vi definere en anden evaluator:

ser lidt ad hoc ud, hvad hvis du har dybt indlejrede udtryk?

Ja, for vilkårlig indlejret udtryk er denne tilgang ikke skalerbar — hvert yderligere nesting niveau kræver, at du skriver specialiseret funktion.

der er en måde at generalisere denne nesting med en ny type:

reparere? Ligner en rekursiv datastruktur, der ikke gør meget. Hvordan er det nyttigt?

lad os først se på udtrykket før lighedstegnet: faktisk Fixer en rekursiv datastruktur, der har en type parameter f. Denne parameter har Art * -> * f.eks. tager det også en type parameter. For eksempel kan du ikke konstruere Fix leverer Int eller Bool, det skal være noget som Maybe, List eller… ExpressionF. Derfor introducerede vi typeparameter for ExpressionF. Dernæst efter lighedstegnet har vi en enkelt type konstruktør Fx tager et enkelt argument af typen f (Fix f) hvilket er dybest set et udtryk, der konstruerer f‘s værdi. I tilfælde af Maybe ville det være Maybe (Fix Maybe) og så er det hele pakket med Fxi type Fix Maybe.

typesignaturen er forvirrende at læse i starten, fordi typekonstruktøren kan have samme navn som selve typen plus selvreferencer. Men der er ikke meget mere i det end blot at indpakke en højere ordretype i en datastruktur. unfix er en modsætning til Fx og alt det gør er mønster matching på Fx og returnerer indpakket værdi, ingen big deal.

nu erstatter vi hvert ExpressionFaf vores udtrykstræ med Fix ExpressionF. Bemærk forskellen i at konstruere udtryk med og uden Fx – de er stort set de samme, bortset fra at vi skal forberede Fx $:

den resulterende type af en ‘fast’ version er Fix ExpressionF så vi er tilbage til en rekursiv repræsentation, men nu skal vi bruge unfix funktion for at få vores ikke rekursive datastruktur tilbage.

hvad er fordelene ved at have Fix? Det ser ud til, at det er den samme tilgang som original Expression type, men nu har vi denne underlige Fix og unfix nonsens?

Ja, men vi forsøger at generalisere foldningsprocessen, det kræver introduktion af yderligere abstraktioner, som Fix og Algebra, som vi vil diskutere senere. Bær over med mig, det skulle give mere mening senere.

så vi har vores ‘faste’ datastruktur, hvordan ville evalueringsfunktionen se ud?

givet en Fix ExpressionF det eneste, vi kan gøre med det, er at kalde unfix som producerer ExpressionF (Fix ExpressionF):

den returnerede ExpressionF kan være en af vores ValueF, AddF eller MultF med en Fix ExpressionF som deres typeparameter. Det giver mening at gøre mønster matching og beslutte, hvad de skal gøre næste:

Ja, det ser det samme ud som vores allerførste rekursive evaluator for Expression med tilføjelse af at skulle pakke udtrykket ud med unfix. Så hvorfor gider med Fix alligevel?

her er nøglen: vi vil genbruge vores oprindelige ‘rettelse-mindre’ evaluator for ExpressionF og en eller anden måde distribuere det over Fix ExpressionF stucture. Så dette skal være en funktion, der tager to argumenter-evaluatoren og strukturen til evaluering:

lad os prøve at finde ud af implementeringen — den første logiske ting at gøre er at bruge unfix for at få ExpressionF og så måske sende den til evaluator:

det virker selvfølgelig ikke, evaluator forventer ExpressionF Intog ikke ExpressionF (Fix ExpressionF). Husk forresten, at ExpressionF er en Functor? Det er her, det bliver praktisk — vi kan bruge fmap til at anvende den samme proces på det indre niveau af vores udtrykstræ:

Tag et øjeblik og tænk over, hvad der sker: vi sender en rekursiv funktion almostCata evaluator ind i fmap. Hvis det aktuelle udtryk er AddF eller MultF, vil denne funktion blive bestået et niveau dybere og fmap vil blive kaldt igen. Dette vil ske, indtil vi når ValueF, fmapping over ValueF returnerer værdi af typen ExpressionF Int og det er præcis, hvad vores evaluator funktion accepterer.

ved at se på almostCata kan vi se, at det ikke rigtig har noget specifikt for ExpressionF eller Inttype og teoretisk kan generaliseres med en eller anden type parameter f. Den eneste begrænsning skal have en Functor forekomst for f , fordi vi bruger fmap:

og det er den endelige version af cata. Her er den fulde implementering med nogle brugseksempler:

det er vist sejt. Men hvorfor tho?

mange begreber i kategoriteori og funktionel programmering er ret abstrakte, og nogle gange er det svært at finde øjeblikkelig praktisk anvendelse til en bestemt ide. Men at lede efter abstraktioner og generaliseringer er nyttigt til at finde mønstre og elegante løsninger på problemer, der ellers kræver ad hoc-implementering.

forresten, ved at generalisere vores ExpressionF -> Int funktion til Functor f => (f a -> a) opdagede vi et andet vigtigt koncept kaldet F-Algebra. Grundlæggende er f-Algebra en tredobbelt funktion f, en eller anden type aog evaluatorfunktion f a -> a. Bemærk, at a her ikke polymorfe – det skal være en konkret type, ligesom Int eller Bool og det kaldes en carrier type. For enhver endo-functor f kan du oprette flere F-Algebra er baseret på det. Tag vores udtryk eksempel-endo-functor f er ExpressionF, a er Intog evaluator er evalExprF. Men vi kan ændre transportør typen og producere flere algebraer:

det er bare forskellige evaluatorer, der kan overføres til cata, ikke?

Ja, Vi vælger forskellige transporttyper og vælger vores implementering. Men der er tricket – der er en mor til alle evaluatorer, som vi kan skabe ved at vælge vores transportørtype til at være… Fix ExprF.

evaluering til Int eller Bool giver helt mening, men hvad ville dette initialAlgebra evaluere? Hvornår skal jeg have Fix af noget som følge af min evaluator?

selvfølgelig vil du ikke skrive noget sådan selv, vil bare vise dig den dybere betydning bag f-algebraer og cata. Faktisk har vi allerede en implementering for en sådan evaluator, og det er præcis Fx constructor:

vent, Fx er en evaluator? Det er vanvittigt.

Ja, og det gør det mest enkle, du kan gøre — Gem ekspessionen i en datastruktur. Mens alle andre evaluatorer (algebra0, algebra1) producerede en vis værdi ved at reducere udtrykket (som at gøre sum eller sammenkædning) Fx bare ombryder udtrykket uden at miste nogen data.

derfor introducerede vi Fix i første omgang — du vurderer først din oprindelige datastruktur med Fx i initial algebra Fix f og bruger derefter cataden ‘rigtige’ evaluering sker ved fmap ing din konkrete evaluator over inital algebra.

fra kategoriteori synspunkt danner alle algebraer baseret på den samme endo-functor en kategori. Denne kategori har et indledende objekt, som er vores oprindelige algebra oprettet ved at vælge bæretypen som Fix f. Der er nogle gode blogindlæg af Bartos Milevski, som jeg stærkt anbefaler at tjekke ud, hvis du vil få dyb kategorisk forståelse.

det er stadig ret svært at forstå, Jeg tror ikke, jeg fuldt ud forstår konceptet

det er altid bedre at gøre hænder på: Prøv re-implementering Fix og cata på egen hånd, tænk på mulige datastrukturer og algebraer. For eksempel kan en String repræsenteres rekursivt (som et Char hoved og hale på String), length af en streng kan beregnes med cata. Her er nogle gode ressourcer til yderligere læsning:

• forståelse af F-algebraer og lidt forskellige F-algebraer af Bartos Milevski
• Katamorfismer på 15 minutter af Chris Jones
• ren funktionel Databaseprogrammering med Fikspunkttyper af Rob Norris
• Katamorfismer på Haskell Viki
• praktiske rekursionsordninger ved hjælp af Jared Tobin