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

22

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

functional-programming haskell

— Gaurav Abbi
źródło

@jozefg: Dziękujemy za link do twojego postu. Jedno pytanie na ten temat. W zdaniu „Algebra w tym sensie jest parą obiektu C i mapą FC → C.”, czy C naprawdę ma być przedmiotem, czy raczej kategorią? Innymi słowy, nie jestem pewien, czy F oznacza funktor w kategorii, a algebry F są algebrami indukowanymi przez ten funktor, czy F jest konkretną strzałą od obiektu na siebie.

— Giorgio

Cjest obiektem w jakiejś kategorii (powiedzmy CC), Fjest funktorem, CC -> CCwięc odwzorowuje się z CCpowrotem na sobie. Teraz F CC -> CCjest tylko zwykła strzałka w kategorii CC. Tak więc Falgebra jest przedmiotem C : CCi strzałą F C -> CwCC

— Daniel Gratzer

4

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!

— Klaas van Schelven
źródło

19

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.

— Daniel Gratzer
źródło

2

czy warto wspomnieć, że banany są nawiasami (| |), których oryginalny papier używa do zdefiniowania kata

— jk.

7

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.

— Jackie
źródło