2014-07-22 17 views
13

W opakowaniu recursion-schemes możemy wyrazić to, że (ściśle dodatnie) algebraiczna typ danychDlaczego typ algebraiczny byłby tylko początkową algebrą (lub odwrotnie)?

  1. ma funktor sygnatury, f
  2. jest początkową f -algebra i
  3. jest ostatnim f -coalgebra

na przykład, możemy zrobić dla [a] z następującego kodu

-- (1) define and declare the signature functor, here called Base 

data instance Prim [a] x = Nil | Cons a x deriving Functor 
type instance Base [a] = Prim [a] 

-- (2) demonstrate the initial algebra 
instance Foldable [a] where 
    project []  = Nil 
    project (a:as) = Cons a as 

-- (3) demonstrate the final coalgebra 
instance Unfoldable [a] where 
    embed Nil   = [] 
    embed (Cons a as) = a:as 

W każdym typie, w którym mamy (1), (2) i (3) powinniśmy mieć, że (project, embed) jest świadkiem izomorfizmu.

To moja zrozumienie, że typy danych w dużych (lub przynajmniej surowo-pozytywne) są zawsze ostateczne/CO/początkowy Algebry jakiegoś podpisu funktor w rzeczywistości są one zawsze zarówno.

Moje pytanie brzmi: dlaczego Foldable i są oddzielnymi klasami? Kiedy typ danych byłby tylko jednym lub drugim?

Obecnie mogę sobie wyobrazić, że to może być cenna dla abstrakcyjnych typów danych, które tylko chcą zapewnić albo składanie lub rozkładanie interfejsu, ale są inne czasy, jak również?

+0

Czy musimy koniecznie określić wzajemne algebrę i coalgebra dla wszelkich typów? Czy byłoby możliwe, że dla jakiegoś typu chciałoby się zdefiniować algebrę konstruującą wartości i węgiel do ich przetworzenia (a nie tylko zdekonstruować "dually")? – didierc

+2

Można było na pewno, będzie to oznaczać, że Rozkłada rozwijają się podzbiór możliwych wartości i fałdy „widok” podzbioru możliwe dane, to prawie na pewno wystąpią w abstrakcyjny typ danych (inny dlaczego streszczenie to w ogóle?) . Moja lektura dotycząca zamierzonych znaczeń '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' '' 'bazowy" powinien być dokładnie tym, który jest sygnaturą tego typu i dlatego jest odwrotny. –

+1

Wydaje mi się, że 'Składane' i' Niefoldujące' służą do wyświetlania typów danych odpowiednio jako algebry i węglowe, niekoniecznie początkowe lub końcowe. (Jest to prawdopodobnie co @didierc mówił też.) –

Odpowiedz

5

To nie może być odpowiedzią na pytanie, ale to naprawdę nie jest prawdą, że ściśle dodatnie typy danych Haskell są początkowe algebry. Powodem tego jest to, że nawet w całkowitym podzbiorze Haskella (który jest tym, co chcemy pracować podczas rozumowania!) Macie nieskończone dane.

Przykładowo krotnie listy nieskończonej jest częściowa.

+0

Nie utrzymuję tego napięcia w moim umyśle, ale masz rację. Nie jestem jednak pewien, jak najlepiej to sformułować (i z przyjemnością edytowałbym to pytanie z dowolnymi sugestiami). Chciałbym zasugerować ideę, że najmniej ustalony punkt i największy stały punkt pokrywają się w Haskell, a przynajmniej to, że nie ogranicza cię od przekazania generatora do fałdu. To łamie powszechność, ale nie wiem, jak inaczej to powiedzieć. –

Powiązane problemy