Catamorfismi e F-Algebre

Quindi sento spesso le parole “catamorfismo”e” schemi di ricorsione”. Di che si tratta?

I catamorfismi (o cata) sono generalizzazioni del concetto di piega nella programmazione funzionale. Data una F-Algebra e una struttura dati ricorsiva, un catamorfismo produrrà un valore valutando ricorsivamente la struttura dei dati.

Che cos’è una F-Algebra? Forse puoi mostrare prima alcuni esempi di codice?

La configurazione non è così semplice, quindi iniziamo semplice. Supponiamo di avere la seguente struttura dati per rappresentare un’espressione:

E una semplice espressione può apparire come questo:

Avendo solo un’espressione della struttura di dati è inutile, naturalmente, avrete bisogno di una funzione di valutare e ottenere il risultato:

Questo è dove catamorphism generalizzazione viene in:

🤨, ma qual è il punto? Stai solo applicando un argomento a una funzione?

Questo perché è notReallyCata. La funzione reale cata è generica e non dipende da alcuna particolare struttura di dati o funzione di valutazione. Vedi, la creazione di una struttura dati ricorsiva e quindi il ripiegamento su di essa è un modello comune che cata cerca di generalizzare.

Ok, allora come appare il vero cata?

🤯

Ecco perché abbiamo iniziato con notReallyCata. Abbatteremo l’implementazione più tardi fino a quando non scatta. Ma ora continuiamo con il nostro esempio Expression. Innanzitutto, dobbiamo sbarazzarci della ricorsione introducendo un parametro di tipo:

Tutti i riferimenti a Expression vengono sostituiti con il parametro di tipo a in modo che la struttura dei dati non sia più ricorsiva.

Perché c’è un F alla fine dei costruttori di tipi?

Contento che tu abbia chiesto — questo è un suggerimento che ExpressionF può essere un Functor:

Niente di speciale, basta applicare alcune funzioni al valore avvolto preservando la struttura.

Non sono sicuro del motivo per cui ne abbiamo bisogno 🤔

Non ha senso ora, ma lo farà un po ‘ più tardi. Ora, il modo in cui creiamo la nostra espressione non è cambiato (ad eccezione dei nomi dei costruttori):

Ma il tipo risultante è diverso:

expr comprime tutto in un unico Expression mentre exprF codifica le informazioni sul livello di nidificazione del nostro albero delle espressioni. Parlando di valutazione, questo è il modo in cui possiamo implementare eval per ExpressionF:

La differenza principale con l’originale evalExpr è che non abbiamo una chiamata ricorsiva a evalExprF (ExpressionF non è ricorsiva, ricordi?). Significa anche che il nostro valutatore può lavorare solo con un’espressione a livello singolo:

E non compilerà su questo:

Semplicemente perché exprF expepects ExpressionF Int e stiamo spingendo ExpressionF (ExpressionF Int).

Per farlo funzionare potremmo definire un altro valutatore:

Sembra un po ‘ ad hoc, cosa succede se hai espressioni profondamente annidate?

Sì, per l’espressione annidata arbitraria questo approccio non è scalabile: ogni livello di nidificazione aggiuntivo richiede la scrittura di funzioni specializzate.

C’è un modo per generalizzare questo nesting con un nuovo tipo:

Aggiustare? Sembra una struttura di dati ricorsiva che non fa molto. Come è utile?

Diamo prima un’occhiata all’espressione prima del segno di uguale: infatti Fix è una struttura di dati ricorsiva che ha un parametro di tipo f. Questo parametro ha kind * -> * ad esempio richiede anche un parametro type. Ad esempio, non è possibile costruire Fix fornendo Int o Bool, deve essere qualcosa come Maybe, List o or ExpressionF. Questo è il motivo per cui abbiamo introdotto il parametro type per ExpressionF. Successivamente, dopo il segno di uguale, abbiamo un singolo costruttore di tipo Fx che prende un singolo argomento di tipo f (Fix f)che è fondamentalmente un’espressione che costruisce il valore di f. Nel caso di Maybe sarebbe Maybe (Fix Maybe) e quindi il tutto viene avvolto con Fxnel tipo Fix Maybe.

La firma del tipo è confusa da leggere all’inizio perché il costruttore del tipo può avere lo stesso nome del tipo stesso più auto riferimento. Ma non c’è molto di più che avvolgere un tipo di ordine superiore in una struttura dati. A proposito, unfix è un opposto a Fx e tutto ciò che fa è la corrispondenza del modello su Fx e restituisce il valore avvolto, nessun grosso problema.

Ora, sostituiremo ogni ExpressionF del nostro albero delle espressioni con Fix ExpressionF. Si noti la differenza nella costruzione di espressioni con e senza Fx — sono fondamentalmente la stessa, tranne che dobbiamo anteporre Fx $:

Il tipo risultante di un ‘fisso’ è Fix ExpressionF così siamo di nuovo ad un ricorsiva rappresentazione, ma ora dobbiamo usare unfix funzione per ottenere il nostro non ricorsiva struttura di dati indietro.

Quali sono i vantaggi di avere Fix? Sembra che sia lo stesso approccio del tipo originale Expression ma ora abbiamo questa strana assurdità Fix e unfix?

Sì, ma stiamo cercando di generalizzare il processo di piegatura, richiede l’introduzione di astrazioni aggiuntive, come Fix e Algebra che discuteremo più avanti. Abbi pazienza, dovrebbe avere più senso dopo.

Quindi abbiamo la nostra struttura dati “fissa”, come sarebbe la funzione di valutazione?

Dato un Fix ExpressionF l’unica cosa che possiamo fare è chiamare unfix che produce ExpressionF (Fix ExpressionF):

restituiti ExpressionF può essere uno dei nostri ValueF, AddF o MultF in un Fix ExpressionF come il loro tipo di parametro. Ha senso fare pattern matching e decidere cosa fare dopo:

Sì, sembra lo stesso del nostro primissimo valutatore ricorsivo per Expression con l’aggiunta di dover scartare l’espressione con unfix. Quindi perché preoccuparsi di Fix comunque?

Ecco la chiave: riutilizzeremo il nostro valutatore “fix-less” originale per ExpressionF e in qualche modo lo distribuiremo sulla struttura Fix ExpressionF. Quindi questo dovrebbe essere una funzione che prende due argomenti — il valutatore e la struttura per valutare:

proviamo a capire l’attuazione — la prima cosa logica da fare è usare unfix arrivare ExpressionF e poi magari passare a evaluator:

Ovviamente questo non funziona, evaluator aspetta ExpressionF Int e non ExpressionF (Fix ExpressionF). A proposito, ricorda che ExpressionF è un Functor? Questo è dove diventa utile-possiamo usare fmap per applicare lo stesso processo al livello interno del nostro albero delle espressioni:

Prenditi un momento e pensa a cosa succede: stiamo passando una funzione ricorsiva almostCata evaluator in fmap. Se l’espressione corrente è AddF o MultF, questa funzione verrà superata di un livello più profondo e fmap verrà richiamata di nuovo. Questo accadrà fino a quando non raggiungeremo ValueF, fmapping su ValueF restituisce il valore di tipo ExpressionF Int e questo è esattamente ciò che la nostra funzione evaluator accetta.

Guardando almostCata possiamo vedere che in realtà non ha nulla di specifico per il tipo ExpressionF o Int e teoricamente può essere generalizzato con qualche parametro di tipo f. L’unico vincolo dovrebbe avere un’istanza Functor per f, perché stiamo usando fmap:

E questa è la versione finale di cata. Ecco l’implementazione completa con alcuni esempi di utilizzo:

Immagino sia figo. Ma perché tho?

Molti concetti nella teoria delle categorie e nella programmazione funzionale sono piuttosto astratti e talvolta è difficile trovare un’applicazione pratica immediata per determinate idee. Ma cercare astrazioni e generalizzazioni è utile per trovare modelli e soluzioni eleganti a problemi che altrimenti richiedono un’implementazione ad hoc.

A proposito, generalizzando la nostra funzione ExpressionF -> Int a Functor f => (f a -> a) abbiamo scoperto un altro concetto importante chiamato F-Algebra. Fondamentalmente F-Algebra è una tripla di functor f, un certo tipo ae funzione valutatore f a -> a. Si noti che a qui non polimorfico-deve essere un tipo concreto, come Int o Bool e si chiama tipo portante. Per qualsiasi func-functor f è possibile creare più F-Algebra basate su di esso. Prendi il nostro esempio di espressioni-end-functor f is ExpressionF, a is Inte evaluator is evalExprF. Ma possiamo cambiare il tipo di vettore e produrre più algebre:

Sono solo diversi valutatori che possono essere passati in cata, giusto?

Sì, stiamo scegliendo diversi tipi di carrier e scegliendo la nostra implementazione. Ma c’è il trucco-c’è una madre di tutti i valutatori che possiamo creare scegliendo il nostro tipo di vettore per essere Fix ExprF.

Valutare a Int o Bool ha senso, ma cosa valuterebbe questo initialAlgebra? Quando ho bisogno di avere Fix di qualcosa come risultato del mio valutatore?

Ovviamente non scriverai qualcosa del genere da solo, vuoi solo mostrarti il significato più profondo dietro f-algebre e cata. In effetti, abbiamo già un’implementazione per tale valutatore e questo è esattamente Fx costruttore:

Aspetta, Fx è un valutatore? E ‘ pazzesco.

Sì e fa la cosa più semplice che puoi fare — salva l’expession in una struttura dati. Mentre tutti gli altri valutatori (algebra0, algebra1) hanno prodotto un certo valore riducendo l’espressione (come fare somma o concatenazione) Fx semplicemente avvolge l’espressione senza perdere alcun dato.

Questo è il motivo per cui abbiamo introdotto Fix in primo luogo — per prima cosa valuti la tua struttura dati originale con Fx nell’algebra iniziale Fix f e poi usando catala valutazione “reale” avviene con fmap ing il tuo valutatore concreto sull’algebra iniziale.

Dal punto di vista della teoria delle categorie, tutte le algebre basate sullo stesso func-funtore formano una categoria. Questa categoria ha un oggetto iniziale che è la nostra algebra iniziale creata selezionando il tipo di vettore come Fix f. Ci sono alcuni grandi post del blog di Bartosz Milewski che consiglio vivamente di verificare se si desidera ottenere una profonda comprensione categorica.

È ancora piuttosto difficile da comprendere, non penso di comprendere appieno il concetto

È sempre meglio fare le mani: prova a re-implementare Fix e cata da solo, pensa a possibili strutture dati e algebre. Ad esempio, un String può essere rappresentato ricorsivamente (come Char head e tail di String), il length di una stringa può essere calcolato con cata. Ecco alcune grandi risorse per ulteriori letture:

• Comprensione delle F-algebre e delle F-algebre leggermente diverse di Bartosz Milewski
• Catamorfismi in 15 minuti di Chris Jones
• Programmazione di database funzionali puri con tipi Fixpoint di Rob Norris
• Catamorfismi su Haskell wiki
• Schemi di ricorsione pratici di Jared Tobin