Są domyślnie typem algebry danych haskell?

Question

Próbuję objąć moją głowę algebrami F, a this article wykonuje całkiem niezłą robotę. Rozumiem pojęcie teorii dualnej w kategorii, ale trudno mi zrozumieć, w jaki sposób F-coalgebras (dual-algebr F) odnosi się do leniwych struktur danych w Haskell.

F-algebry opisywane są za pomocą funkcji endofunctor: F a -> a, co ma sens, jeśli myśli się o F a jako wyrażeniu, a także o wyniku oceny tego wyrażenia, jak wyjaśnia objaśniony artykuł to.

Będąc dualią F-algebr, odpowiednia funkcja dla F-węgierki byłaby -> F a. Wikipedia mówi, że F-coalgebras mogą być używane do tworzenia nieskończonych, leniwych struktur danych. W jaki sposób a -> F functon pozwala na tworzenie nieskończonych, leniwych struktur danych? Mając to na uwadze, skoro Haskell jest leniwy, to większość typów danych znajduje się w Haskell F-coalgebrach zamiast F-algebrach? Czy algebry F nie są leniwie oceniane?

Jeśli typy danych (lub co najmniej te, dla których są zdolne do wyświetlania nieskończonych danych) oparte są na F-węglach w Haskell, na przykład funkcja -> F a dla list? Co to jest terminal F-coalgebra dla list?

Dokonywanie nieskończoną listę [1,2,3,4 ...] może wyglądać tak w Haskell:

list = 1 : map (+ 1) list 

robi tego zastosowania F-coalgebras jakoś? Czy nieskończone struktury danych wymagają pojęcia leniwej oceny i rekurencji wraz z użyciem F-coalgebras? Czy coś mi umyka?

Answer 1

Węgiel kamienny A -> F A może zostać użyty do złuszczenia zewnętrznej warstwy (prawdopodobnie nieskończonej) struktury danych. Dla list od X funktor jest F a = Maybe (X, a), taki sam jak w widoku algebraicznym. Haskell funkcję w coalgebra jest

headView :: [a] -> Maybe (a, [a]) 
headView [] = Nothing 
headView (x:xs) = Just (x,xs) 

unfoldr jest rozwinięć odpowiadający tej coalgebra, jak foldr jest składana odpowiadający tej Algebra.

Jeśli uważasz, że [a] nie jako typ list, ale jako typ opisów list lub programów, to pozwala ci konstruować (na pozór) nieskończone wartości, tylko z koniecznym skończonym opisem.

Jak widać, lista Haskell wygląda zarówno jako algebra F, jak i F-węgierska. Jest to możliwe, ponieważ Haskell nie jest w rzeczywistości spójny. Możesz spasować i rozwinąć nieskończoną pętlę. Języki takie jak coq i agda wyraźnie rozróżniają typy danych (F-algebras) i typy kodów (F-coalgebras). W tych językach masz dwa typy list: algebraiczny List i węgielgebraiczny Colist.