Co to jest podział i łączenie bananów w programowaniu funkcjonalnym?

Warunki te zostały wymienione na moim kursie uniwersyteckim. Szybkie wyszukiwanie w Google wskazało mi kilka prac uniwersyteckich, ale szukam prostego wyjaśnienia.

Mimo że udzielono już 2 odpowiedzi, nie sądzę, aby wyjaśniono tu „podział bananów”.

Jest to rzeczywiście zdefiniowane w „Funkcjonalnym programowaniu z bananami, soczewkami, kopertami i drutem kolczastym, Erik Meijer Maarten Fokkinga, Ross Paterson, 1991”; ten artykuł jest trudny do przeczytania (dla mnie) ze względu na intensywne stosowanie Squiggola. Jednak „Samouczek na temat uniwersalności i ekspresji składania, Graham Hutton, 1999” zawiera definicję, która jest łatwiejsza do przeanalizowania:

Jako prosty pierwszy przykład użycia zagięcia do generowania krotek, rozważ funkcję sumlength, która oblicza sumę i długość listy liczb:

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

Dzięki prostej kombinacji definicji sumy i długości funkcji za pomocą funkcji składania podanej wcześniej, funkcję sumlength można przedefiniować jako pojedyncze zastosowanie funkcji fold, która generuje parę liczb z listy liczb:

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

Ta definicja jest bardziej wydajna niż pierwotna definicja, ponieważ powoduje tylko jedno przejście przez listę argumentów, a nie dwa oddzielne przejścia. Uogólniając z tego przykładu, każdą parę aplikacji fold na tej samej liście można zawsze łączyć, aby dać pojedyncze zastosowanie fold, które generuje parę, odwołując się do tak zwanej właściwości fold fold ( split banana) (Meijer, 1992) . Dziwna nazwa tej właściwości wynika z faktu, że operator składania jest czasami zapisywany za pomocą nawiasów (| |), które przypominają banany, a operator parowania jest czasem nazywany split. Dlatego ich kombinację można nazwać split bananem!

Jest to tak naprawdę odniesienie do artykułu Meijera i kilku innych zatytułowanych „ Programowanie funkcjonalne z bananami, soczewkami, kopertami i drutem kolczastym ”, podstawową ideą jest to, że możemy wziąć dowolny typ danych rekurencyjnych, jak powiedzmy

 data List = Cons Int List | Nil

i możemy rozliczyć rekurencję na zmienną typu

 data ListF a = Cons Int a | Nil

powodem, dla którego dołączyłem, Fjest to, że jest to teraz funkt! Pozwala nam także naśladować listy, ale z pewnym zwrotem: aby budować listy, musimy zagnieżdżać typ listy

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

Aby odzyskać naszą oryginalną listę, musimy zagnieżdżać ją w nieskończoność . To da nam typ ListFFgdzie

  ListF ListFF == ListFF

W tym celu zdefiniuj „stały typ punktu”

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

Jako ćwiczenie powinieneś sprawdzić, czy spełnia to powyższe równanie, a teraz możemy wreszcie zdefiniować, czym są banany (katamorfizmy)!

  type ListAlg a = ListF a -> a

ListAlgs są rodzajem „algebr listowych” i możemy zdefiniować określoną funkcję

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

Ponadto

  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

Wygląda podobnie? catajest dokładnie taki sam jak prawe fałdy!

Naprawdę interesujące jest to, że możemy to zrobić na więcej niż tylko listach, każdy typ zdefiniowany za pomocą tego „stałego punktu funktora” ma catai, aby pomieścić je wszystko, wystarczy rozluźnić podpis typu

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

Jest to faktycznie zainspirowane fragmentem teorii kategorii, o której pisałem , ale jest to mięso strony Haskella.

Chociaż jozefg udzielił odpowiedzi, nie jestem pewien, czy odpowiedział na pytanie. „Prawo syntezy jądrowej” wyjaśniono w następującym artykule:

Samouczek na temat uniwersalności i ekspresji składania, GRAHAM HUTTON, 1999

Zasadniczo mówi, że w niektórych warunkach można łączyć („utrwalać”) kompozycję funkcji i składać w jedną fałdę, więc w zasadzie

h · fold gw = fold fv

Warunki dla tej równości są

hw = v
h (gxy) = fx (hy)

„Podział banana” lub „zasada podziału banana” pochodzi z artykułu

Programowanie funkcjonalne z bananami, soczewkami, kopertami i drutem kolczastym, Erik Meijer Maarten Fokkinga, Ross Paterson, 1991

Niestety artykuł jest bardzo trudny do rozszyfrowania, ponieważ wykorzystuje formalizm Bird – Meertens, więc nie mogłem zrobić z niego głowy ani ogona. O ile rozumiem „prawo podziału bananów”, mówi ono, że jeśli masz 2 fałdy działające na tym samym argumencie, można je scalić w jeden fałd.