Catamorfismen en F-algebra ‘ s

zo hoor ik vaak de woorden “catamorfisme” en “recursieschema ‘ s”. Waar gaat dat over?

Catamorfismen (of cata) zijn generalisaties van het concept van een vouw in functioneel programmeren. Gegeven een F-Algebra en een recursieve gegevensstructuur zal een catamorfisme een waarde produceren door recursief uw gegevensstructuur te evalueren.

Wat is een F-Algebra? Misschien kun je eerst wat codevoorbeelden laten zien?

de instelling is niet zo eenvoudig dus laten we eenvoudig beginnen. Laten we zeggen dat je moet de onderstaande gegevensstructuur hebben voor het vertegenwoordigen van een expressie:

En een eenvoudige uitdrukking kan er als volgt uitzien:

het Hebben van slechts een uitdrukking data structuur is nutteloos, natuurlijk moet je je een functie te evalueren en het resultaat:

Dit is waar catamorphism generalisatie komt in:

🤨, maar wat is het punt? Je past gewoon een argument toe op een functie?

dat komt omdat het notReallyCatais. De reële cata – functie is generiek en is niet afhankelijk van een bepaalde gegevensstructuur of evaluatorfunctie. Zie, het aanmaken van een recursieve datastructuur en er dan over vouwen is een algemeen patroon dat cata probeert te generaliseren.

Ok, hoe ziet de echte cata er dan uit?

🤯

daarom zijn we begonnen met notReallyCata. We breken de implementatie later af tot het klikt. Maar laten we nu verder gaan met ons Expression voorbeeld. Eerst moeten we van recursie afkomen door een type parameter te introduceren:

alle verwijzingen naar Expression worden vervangen door a typeparameter, zodat de gegevensstructuur niet langer recursief is.

Waarom is er een F aan het einde van type constructeurs?

blij dat u het vroeg-dat is een hint dat ExpressionF een Functor:

niets bijzonders, gewoon een functie toepassen op de verpakte waarde behoud stuctuur.

niet zeker waarom we dat nodig hebben 🤔

het slaat nu nergens op, maar dat komt later wel. De manier waarop we onze expressie creëren is niet veranderd (behalve voor constructornamen):

maar het resulterende type is anders:

expr vouwt alles op in een enkele Expression terwijl exprF informatie codeert over het nestniveau van onze expressieboom. Over evaluatie gesproken, Dit is hoe we kunnen gaan over het implementeren van evaluatie voor ExpressionF:

het belangrijkste verschil met origineel evalExpr is dat we geen recursieve aanroep hebben naar evalExprF (ExpressionF is niet recursief, Weet je nog?). Het betekent ook dat onze evaluator alleen kan werken met een enkele Level expressie:

en zal niet compileren op deze:

simpelweg omdat exprF verwacht ExpressionF Int en we ExpressionF (ExpressionF Int)duwen.

om het te laten werken zouden we een andere evaluator kunnen definiëren:

ziet er ad hoc uit, wat als je diep geneste uitdrukkingen hebt?

Ja, voor willekeurige geneste expressie is deze benadering niet schaalbaar — elk extra nestelniveau vereist dat u een gespecialiseerde functie schrijft.

er is een manier om deze nesting te generaliseren met een nieuw type:

repareren? Lijkt op een recursieve datastructuur die niet veel doet. Hoe is het nuttig?

laten we eerst kijken naar de expressie voor het gelijk-teken: indeed Fix is een recursieve gegevensstructuur die één type parameter fheeft. Deze parameter heeft Soort * -> *, bijvoorbeeld het heeft ook een type parameter. U kunt bijvoorbeeld Fix niet construeren met Int of Bool, het moet iets zijn als Maybe, List of … ExpressionF. Daarom introduceerden we type parameter voor ExpressionF. Vervolgens, na het gelijkteken hebben we een enkele type constructor Fx die een enkel argument van type f (Fix f) neemt, wat in principe een uitdrukking is die de waarde van fconstrueert. In het geval van Maybe zou het Maybe (Fix Maybe) zijn en dan wordt het geheel met Fx omwikkeld in type Fix Maybe.

de typehandtekening is in het begin verwarrend om te lezen omdat type constructor dezelfde naam kan hebben als het type zelf plus zelfreferencing. Maar er is niet veel meer aan de hand dan alleen het verpakken van een hogere orde type in een gegevensstructuur. Btw, unfix is een tegengesteld aan Fx en alles wat het doet is pattern matching op Fx en retourneert wrapped waarde, geen big deal.

nu zullen we elke ExpressionF van onze expressieboom vervangen door Fix ExpressionF. Merk het verschil op in het construeren van expressies met en zonder Fx — ze zijn in principe hetzelfde, behalve dat we voorvoegsel moeten maken Fx $:

het resulterende type van een’ vaste ‘ versie is Fix ExpressionF dus we zijn terug bij een recursieve representatie, maar nu moeten we de unfix functie gebruiken om onze niet recursieve datastructuur terug te krijgen.

Wat zijn de voordelen van Fix? Het lijkt erop dat het dezelfde aanpak is als het originele Expression type maar nu hebben we deze rare Fix en unfix onzin?

Ja, maar we proberen het proces van vouwen te veralgemenen, het vereist introductie van extra abstracties, zoals Fix en Algebra die we later zullen bespreken. Wacht even, het zal later logischer worden.

dus we hebben onze ‘vaste’ gegevensstructuur, hoe zou de evaluatiefunctie eruit zien?

gegeven een Fix ExpressionF het enige wat we kunnen doen met het is het aanroepen van unfix die produceert ExpressionF (Fix ExpressionF):

de geretourneerde ExpressionF kan een van onze ValueF, AddF of MultF zijn met een Fix ExpressionF als hun type parameter. Het is zinvol om te doen patroon matching en beslissen wat te doen volgende:

Ja, het ziet er hetzelfde uit als onze allereerste recursieve evaluator voor Expression met toevoeging van het uitpakken van de expressie met unfix. Waarom zou je je dan druk maken over Fix?

hier is de sleutel: we zullen onze originele ‘fix-less’ evaluator voor ExpressionF hergebruiken en op de een of andere manier distribueren over de Fix ExpressionF structuur. Dus dit moet een functie die twee argumenten-de evaluator en de structuur te evalueren:

laten we proberen de implementatie te achterhalen — het eerste logische ding om te doen is om unfix te gebruiken om ExpressionF te krijgen en dan misschien door te geven aan evaluator:

dit werkt duidelijk niet, evaluator verwacht ExpressionF Inten niet ExpressionF (Fix ExpressionF). Weet je nog dat ExpressionF een Functoris? Dit is waar het handig wordt — we kunnen fmap gebruiken om hetzelfde proces toe te passen op het innerlijke niveau van onze expressieboom:

denk even na over wat er gebeurt: we geven een recursieve functie almostCata evaluator door naar de fmap. Als de huidige expressie AddF of MultF is, wordt deze functie een niveau dieper doorgegeven en wordt fmap opnieuw aangeroepen. Dit zal gebeuren totdat we ValueF bereiken, fmapping over ValueF geeft de waarde van het type ExpressionF Int terug en dat is precies wat onze evaluator functie accepteert.

door te kijken naar almostCata kunnen we zien dat het niet echt iets specifieks heeft voor ExpressionF of Int type en theoretisch kan worden gegeneraliseerd met een type parameter f. De enige beperking zou een Functor instantie moeten hebben voor f, omdat we fmap:

en dat is de definitieve versie van cata. Hier is de volledige implementatie met enkele gebruiksvoorbeelden:

ik denk dat dat cool is. Maar waarom tho?

veel concepten in de categorietheorie en functioneel programmeren zijn vrij abstract en soms is het moeilijk om directe praktische toepassing voor bepaalde ideeën te vinden. Maar het zoeken naar abstracties en generalisaties is nuttig voor het vinden van patronen en elegante oplossingen voor problemen die anders ad-hoc implementatie vereisen.

trouwens, door onze ExpressionF -> Int functie te veralgemenen naar Functor f => (f a -> a) ontdekten we een ander belangrijk concept genaamd F-Algebra. In principe is F-Algebra een triple van functor f, een type a en evaluatorfunctie f a -> a. Merk op dat a hier niet polymorf is — het moet een betontype zijn, zoals Int of Bool en het wordt een dragertype genoemd. Voor elke endo-functor f kunt u op basis daarvan meerdere F-Algebra ‘ s maken. Neem ons voorbeeld-endo-functor f is ExpressionF, a is Int en evaluator is evalExprF. Maar we kunnen het dragertype veranderen en meer algebra ‘ s produceren:

dat zijn gewoon verschillende evaluatoren die kunnen worden doorgegeven aan cata, toch?

Ja, we kiezen verschillende carrier types en kiezen onze implementatie. Maar daar is de truc — er is een moeder van alle evaluatoren die we kunnen creëren door het kiezen van ons carrier type te zijn… Fix ExprF.

evalueren tot Int of Bool is volkomen logisch, maar wat zou deze initialAlgebra evalueren? Wanneer moet ik Fix van iets hebben als resultaat van mijn evaluator?

natuurlijk schrijf je zoiets niet zelf, alleen wil je de diepere betekenis achter f-algebra ‘ s en cata laten zien. In feite hebben we al een implementatie voor een dergelijke evaluator en dat is precies Fx constructor:

wacht, Fx is een evaluator? Dat is gek.

Ja en het doet het meest eenvoudige wat u kunt doen — sla de expession op in een gegevensstructuur. Terwijl alle andere beoordelaars (algebra0, algebra1) enige waarde produceerden door de uitdrukking te verminderen (zoals som of samenvoeging) Fx de uitdrukking gewoon omwikkelt zonder gegevens te verliezen.

dit is de reden waarom we Fix in de eerste plaats introduceerden — u evalueert eerst uw oorspronkelijke gegevensstructuur met Fx in de initiële algebra Fix f en vervolgens met cata de ‘echte’ evaluatie gebeurt door fmaping uw concrete evaluator over de initale algebra.

vanuit het oogpunt van de categorietheorie vormen alle algebra ‘ s op basis van dezelfde endo-functor een categorie. Deze categorie heeft een initiaal object dat onze initiële algebra is, gemaakt door het dragertype als Fix fte kiezen. Er zijn een aantal geweldige blog posts door Bartosz Milewski die ik sterk aanbevelen het controleren als je wilt diep categorisch begrip te krijgen.

het is nog steeds moeilijk te begrijpen, Ik denk niet dat ik het concept

volledig begrijp het is altijd beter om hands on te doen: probeer Fix en cata zelf opnieuw te implementeren, denk na over mogelijke datastructuren en algebra ‘ s. Bijvoorbeeld, een String kan recursief worden weergegeven (als een Char kop en staart van String), de length van een tekenreeks kan worden berekend met cata. Hier zijn een aantal grote middelen voor verder lezen:

• begrip van F-algebra ‘s en enigszins verschillende F-algebra’ s door Bartosz Milewski
• Catamorfismen in 15 minuten door Chris Jones
• Pure functionele Database programmering met Fixpoint Types door Rob Norris
• Catamorfismen op Haskell wiki
• praktische recursie schema ‘ s door Jared Tobin