Che cos'è la suddivisione delle banane e la fusione nella programmazione funzionale?

Anche se sono già state fornite 2 risposte, non penso che il "split delle banane" sia stato già spiegato qui.

È effettivamente definito in "Programmazione funzionale con banane, lenti, buste e filo spinato, Erik Meijer Maarten Fokkinga, Ross Paterson, 1991"; quell'articolo è difficile da leggere (per me) a causa del suo uso pesante di Squiggol. Tuttavia, "Un tutorial sull'universalità e l'espressività della piega, Graham Hutton, 1999" contiene una definizione che è più facile da analizzare:

As a simple first example of the use of fold to generate tuples, consider the function sumlength that calculates the sum and length of a list of numbers:

sumlength :: [Int] → (Int,Int)
sumlength xs = (sum xs, length xs)

By a straightforward combination of the definitions of the functions sum and length using fold given earlier, the function sumlength can be redefined as a single application of fold that generates a pair of numbers from a list of numbers:

sumlength = fold (λn (x, y) → (n + x, 1 + y)) (0, 0)

This definition is more efficient than the original definition, because it only makes a single traversal over the argument list, rather than two separate traversals. Generalising from this example, any pair of applications of fold to the same list can always be combined to give a single application of fold that generates a pair, by appealing to the so-called ‘banana split’ property of fold (Meijer, 1992). The strange name of this property derives from the fact that the fold operator is sometimes written using brackets (| |) that resemble bananas, and the pairing operator is sometimes called split. Hence, their combination can be termed a banana split!

Quindi questo è in realtà un riferimento a un documento di Meijer e ad alcuni altri chiamato " Programmazione funzionale con banane, lenti, buste e Barbed Wire ", l'idea di base è che possiamo prendere qualsiasi tipo di dati ricorsivo, come ad esempio

 data List = Cons Int List | Nil

e possiamo calcolare la ricorsione in una variabile di tipo

 data ListF a = Cons Int a | Nil

il motivo per cui ho aggiunto che F è perché ora è un funtore! Ci permette anche di imitare le liste, ma con una svolta: per costruire liste dobbiamo nidificare il tipo di lista

type ThreeList = ListF (ListF (ListF Void)))

Per recuperare il nostro elenco originale, dobbiamo continuare a nidificare questo infinitamente . Questo ci darà un tipo ListFF dove

  ListF ListFF == ListFF

Per fare ciò definisci un "tipo di punto fisso"

  data Fix f = Fix {unfix :: f (Fix f)}
  type ListFF = Fix ListF

Come esercizio, dovresti verificare che questo soddisfi la nostra equazione di cui sopra. Ora possiamo finalmente definire cosa sono le banane (catamorfismi)!

  type ListAlg a = ListF a -> a

ListAlg s è il tipo di "lista algebre" e possiamo definire una funzione particolare

  cata :: ListAlg a -> ListFF -> a
  cata f = f . fmap (cata f) . unfix

Altro ancora

  cata :: ListAlg a -> ListFF -> a
  cata :: (Either () (Int, a) -> a) -> ListFF -> a
  cata :: (() -> a) -> ((Int, a) -> a) -> ListFF -> a
  cata :: a -> (Int -> a -> a) -> ListFF -> a
  cata :: (Int -> a -> a) -> a -> [Int] -> a

Hai un aspetto familiare? cata è esattamente uguale a right folds!

Ciò che è veramente interessante è che possiamo fare questo oltre un semplice elenco, qualsiasi tipo definito con questo "punto fisso di un functor" ha un cata e per accedervi tutti dobbiamo solo rilassare la firma del tipo

  cata :: (f a -> a) -> Fix f -> a

Questo in realtà è ispirato da un pezzo di teoria delle categorie che ho scritto su , ma questa è la carne del lato Haskell.

Sebbene jozefg abbia fornito una risposta, non sono sicuro che abbia risposto alla domanda. La "legge sulla fusione" è spiegata nel seguente articolo:

A tutorial on the universality and expressiveness of fold, GRAHAM HUTTON, 1999

Fondamentalmente dice che in alcune condizioni puoi combinare ("fondere") la composizione di una funzione e piegarla in una singola piega, quindi in pratica

h · fold g w = fold f v

Le condizioni per questa uguaglianza sono

h w = v
h (g x y) = f x (h y)

La "banana split" o "banana split law" proviene dall'articolo

Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, Erik Meijer Maarten Fokkinga, Ross Paterson, 1991

Purtroppo l'articolo è molto difficile da decifrare poiché utilizza il formalismo Bird-Meertens quindi non ho potuto fare la testa o la coda di esso. Per quanto ho capito, la "legge sulla banana split" dice che se hai 2 pieghe che funzionano sullo stesso argomento, possono essere unite in un'unica piega.