Słyszałem kilka razy termin „węgiel kamienny” w programowaniu funkcjonalnym i kręgach PLT, szczególnie gdy dyskusja dotyczy przedmiotów, comonad, soczewek itp. Googlowanie tego terminu daje strony, które zawierają matematyczny opis tych struktur, co jest dla mnie prawie niezrozumiałe. Czy ktoś może wyjaśnić, co oznaczają węgiel drzewny w kontekście programowania, jakie jest ich znaczenie i jak odnoszą się do obiektów i comonad?

Algebry

Myślę, że punktem wyjścia byłoby zrozumienie idei algebry . To tylko uogólnienie struktur algebraicznych, takich jak grupy, pierścienie, monoidy i tak dalej. Przez większość czasu te rzeczy są wprowadzane w postaci zestawów, ale ponieważ jesteśmy wśród przyjaciół, będę rozmawiać o typach Haskell. (Nie mogę się jednak oprzeć użyciu greckich liter - sprawiają, że wszystko wygląda fajniej!)

Algebra jest więc typem τz pewnymi funkcjami i tożsamościami. Funkcje te przyjmują różną liczbę argumentów typu τi generują τ: bez pośpiechu, wszystkie wyglądają (τ, τ,…, τ) → τ. Mogą również mieć „tożsamość” - elementy τ, które zachowują się w określony sposób z niektórymi funkcjami.

Najprostszym tego przykładem jest monoid. Monoid to dowolny typ τz funkcją mappend ∷ (τ, τ) → τi tożsamością mzero ∷ τ. Inne przykłady obejmują takie rzeczy jak grupy (które są jak monoidy, z wyjątkiem dodatkowej invert ∷ τ → τfunkcji), pierścienie, siatki i tak dalej.

Wszystkie funkcje działają, τale mogą mieć różne arie. Możemy zapisać je jako τⁿ → τ, gdzie τⁿmapy do krotki n τ. W ten sposób sensowne jest myślenie o tożsamości jako o τ⁰ → τmiejscu, w którym τ⁰jest tylko pusta krotka (). Możemy więc teraz uprościć pomysł algebry: jest to po prostu jakiś typ z pewną liczbą funkcji.

Algebra to po prostu powszechny wzorzec w matematyce, który został „wyodrębniony”, tak jak robimy to z kodem. Ludzie zauważyli, że cała masa interesujących rzeczy - wspomniane monoidy, grupy, kraty itd. - wszystkie mają podobny wzór, więc wyodrębnili go. Zaleta robienia tego jest taka sama, jak w przypadku programowania: tworzy dowody wielokrotnego użytku i ułatwia pewne rodzaje rozumowania.

Algebry F.

Jednak jeszcze nie skończyliśmy z faktoringiem. Do tej pory mamy wiele funkcji τⁿ → τ. Możemy właściwie zrobić sztuczkę, aby połączyć je wszystkie w jedną funkcję. W szczególności spójrzmy na monoidy: mamy mappend ∷ (τ, τ) → τi mempty ∷ () → τ. Możemy zamienić je w jedną funkcję za pomocą typu sumy— Either. Wyglądałoby to tak:

op ∷ Monoid τ ⇒ Either (τ, τ) () → τ
op (Left (a, b)) = mappend (a, b)
op (Right ())    = mempty

Możemy faktycznie korzysta z tej transformacji wielokrotnie łączyć wszystkie te τⁿ → τfunkcje w jeden, dla dowolnej algebry. (W rzeczywistości, możemy zrobić to dla dowolnej liczby funkcji a → τ, b → τi tak dalej za każdy a, b,… ).

To pozwala nam mówić o algebrach jako typach τz jedną funkcją, od pewnego bałaganu Eithers do jednego τ. Dla monoids ten bałagan jest: Either (τ, τ) (); dla grup (które mają dodatkowe τ → τdziałanie), to jest: Either (Either (τ, τ) τ) (). Jest to inny typ dla każdej innej struktury. Co więc mają wspólnego wszystkie te typy? Najbardziej oczywistą rzeczą jest to, że wszystkie są tylko sumami produktów - algebraicznymi typami danych. Na przykład dla monoidów możemy utworzyć argument typu monoid, który działa dla dowolnego monoidu τ:

data MonoidArgument τ = Mappend τ τ -- here τ τ is the same as (τ, τ)
                      | Mempty      -- here we can just leave the () out

Możemy zrobić to samo dla grup, pierścieni, krat i wszystkich innych możliwych struktur.

Co jeszcze jest specjalnego w tych wszystkich typach? Cóż, oni wszyscy Functors! Na przykład:

instance Functor MonoidArgument where
  fmap f (Mappend τ τ) = Mappend (f τ) (f τ)
  fmap f Mempty        = Mempty

Abyśmy mogli jeszcze bardziej uogólnić naszą ideę algebry. To tylko jakiś typ τz funkcją f τ → τfunktora f. W rzeczywistości moglibyśmy zapisać to jako klasę:

class Functor f ⇒ Algebra f τ where
  op ∷ f τ → τ

Jest to często nazywane „algebrą F”, ponieważ jest określane przez funktor F. Gdybyśmy mogli częściowo zastosować klasy, moglibyśmy zdefiniować coś takiego class Monoid = Algebra MonoidArgument.

Coalgebras

Mam nadzieję, że dobrze orientujesz się, czym jest algebra i jak to jest po prostu uogólnienie normalnych struktur algebraicznych. Czym jest F-carbongebra? Cóż, co implikuje, że jest to „dualność” algebry - to znaczy bierzemy algebrę i przerzucamy kilka strzałek. Widzę tylko jedną strzałkę w powyższej definicji, więc po prostu odwrócę to:

class Functor f ⇒ CoAlgebra f τ where
  coop ∷ τ → f τ

I to wszystko! Wniosek ten może wydawać się nieco niepoprawny (heh). Mówi ci, czym jest carbongebra, ale tak naprawdę nie daje wglądu w to, jak jest przydatny i dlaczego nas to obchodzi. Dojdę do tego za chwilę, kiedy znajdę lub wymyślę dobry przykład lub dwa: P.

Klasy i przedmioty

Po krótkiej lekturze wydaje mi się, że mam dobry pomysł, jak używać węgielników do reprezentowania klas i obiektów. Mamy typ, Cktóry zawiera wszystkie możliwe wewnętrzne stany obiektów w klasie; sama klasa jest węgielnicą, w Cktórej określa się metody i właściwości obiektów.

Jak pokazano w przykładzie algebry, jeśli mamy kilka funkcji takich jak a → τi b → τdla dowolnej a, b,…, możemy połączyć je wszystkie w jedną funkcję za Eitherpomocą typu sumy. Podwójny „pojęcie” będzie łącząc kilka funkcji typu τ → a, τ → bi tak dalej. Możemy to zrobić za pomocą dualu typu suma - typ produktu. Biorąc pod uwagę dwie powyższe funkcje (wywołane fi g), możemy utworzyć jedną taką:

both ∷ τ → (a, b)
both x = (f x, g x)

Ten typ (a, a)jest funktorem w prosty sposób, więc z pewnością pasuje do naszego pojęcia „F-carbongebra”. Ta szczególna sztuczka pozwala nam spakować kilka różnych funkcji - lub, w przypadku OOP, metod - w jedną funkcję typu τ → f τ.

Elementy naszego typu Creprezentują wewnętrzny stan obiektu. Jeśli obiekt ma pewne czytelne właściwości, muszą być w stanie zależeć od stanu. Najbardziej oczywistym sposobem na to jest uczynienie ich funkcją C. Więc jeśli chcemy mieć właściwość length (np. object.length), Mielibyśmy funkcję C → Int.

Chcemy metod, które mogą przyjmować argument i modyfikować stan. Aby to zrobić, musimy wziąć wszystkie argumenty i stworzyć nowy C. Wyobraźmy sobie setPositionmetodę, która trwa xi ywspółrzędnych: object.setPosition(1, 2). To będzie wyglądać następująco: C → ((Int, Int) → C).

Ważnym wzorem jest tutaj to, że „metody” i „właściwości” obiektu przyjmują sam obiekt jako swój pierwszy argument. To jest tak samo jak selfparametr w Pythonie i jak domniemane thiswiele innych języków. Coalgebra zasadniczo tylko oddaje zachowanie biorąc selfparametr: to właśnie pierwsza Cw C → F Cto.

Złóżmy to wszystko razem. Wyobraźmy sobie klasę z positionwłaściwością, namewłaściwością i setPositionfunkcją:

class C
  private
    x, y  : Int
    _name : String
  public
    name        : String
    position    : (Int, Int)
    setPosition : (Int, Int) → C

Potrzebujemy dwóch części do reprezentowania tej klasy. Po pierwsze, musimy przedstawić wewnętrzny stan obiektu; w tym przypadku zawiera tylko dwa Intsi a String. (To jest nasz typ C.) Następnie musimy wymyślić carbongebra reprezentującą klasę.

data C = Obj { x, y  ∷ Int
             , _name ∷ String }

Mamy dwie właściwości do napisania. Są dość trywialne:

position ∷ C → (Int, Int)
position self = (x self, y self)

name ∷ C → String
name self = _name self

Teraz musimy tylko móc zaktualizować pozycję:

setPosition ∷ C → (Int, Int) → C
setPosition self (newX, newY) = self { x = newX, y = newY }

To jest jak klasa Python z wyraźnymi selfzmiennymi. Teraz, gdy mamy wiele self →funkcji, musimy połączyć je w jedną funkcję dla funkcji węgla. Możemy to zrobić za pomocą prostej krotki:

coop ∷ C → ((Int, Int), String, (Int, Int) → C)
coop self = (position self, name self, setPosition self)

Typ ((Int, Int), String, (Int, Int) → c)-dla dowolny c -jest funktor, więc coopma formę chcemy: Functor f ⇒ C → f C.

Biorąc to pod uwagę, Cwraz z coopformą carbongebra, która określa klasę, którą podałem powyżej. Możesz zobaczyć, w jaki sposób możemy użyć tej samej techniki do określenia dowolnej liczby metod i właściwości dla naszych obiektów.

To pozwala nam używać rozumowania węgielgebraicznego do radzenia sobie z klasami. Na przykład możemy wprowadzić pojęcie „homomorfizmu F-carbongebra” do reprezentowania przekształceń między klasami. Jest to przerażająco brzmiący termin, który oznacza po prostu transformację między węgielnicami, która zachowuje strukturę. To znacznie ułatwia myślenie o mapowaniu klas na inne klasy.

Krótko mówiąc, F-węgiel reprezentuje klasę, posiadając szereg właściwości i metod, które wszystkie zależą od selfparametru zawierającego stan wewnętrzny każdego obiektu.

Inne kategorie

Do tej pory mówiliśmy o algebrach i węgielach jako typach Haskella. Algebra jest tylko typem τz funkcją, f τ → τa carbongebra jest tylko typem τz funkcją τ → f τ.

Jednak nic tak naprawdę łączy te pomysły Haskell per se . W rzeczywistości są one zwykle wprowadzane w kategoriach zbiorów i funkcji matematycznych, a nie typów i funkcji Haskella. Rzeczywiście, możemy uogólnić te pojęcia na dowolne kategorie!

Możemy zdefiniować algebrę F dla jakiejś kategorii C. Po pierwsze, potrzebujemy funktora F : C → C- to znaczy endofunkturza . (Wszystko Haskell Functors faktycznie endofunctors z Hask → Hask). Następnie, algebra jest tylko obiekt Aod Cz morfizmu F A → A. Węgiel jest taki sam, z wyjątkiem A → F A.

Co zyskujemy, rozważając inne kategorie? Cóż, możemy wykorzystać te same pomysły w różnych kontekstach. Jak monady. W Haskell monada jest rodzajem M ∷ ★ → ★z trzema operacjami:

map      ∷ (α → β) → (M α → M β)
return   ∷ α → M α
join     ∷ M (M α) → M α

Ta mapfunkcja jest tylko dowodem na to, że Mjest to Functor. Możemy więc powiedzieć, że monada to po prostu funktor z dwiema operacjami: returni join.

Functory same tworzą kategorię, a morfizmy między nimi są tak zwanymi „naturalnymi przemianami”. Naturalna transformacja jest tylko sposobem na przekształcenie jednego funktora w inny, przy jednoczesnym zachowaniu jego struktury. Oto fajny artykuł, który pomaga wyjaśnić ten pomysł. Mówi o tym concat, co dotyczy tylko joinlist.

W przypadku funktorów Haskell skład dwóch funktorów jest sam funktorem. W pseudokodzie możemy napisać to:

instance (Functor f, Functor g) ⇒ Functor (f ∘ g) where
  fmap fun x = fmap (fmap fun) x

Pomaga nam to myśleć o joinmapowaniu f ∘ f → f. Rodzaj joinjest ∀α. f (f α) → f α. Intuicyjnie możemy zobaczyć, jak funkcję poprawną dla wszystkich typów αmożna traktować jako transformację f.

returnjest podobną transformacją. Jego typ to ∀α. α → f α. Wygląda to inaczej - pierwszy αnie jest funktorem! Na szczęście, możemy rozwiązać ten problem przez dodanie istnieje funktor tożsamości: ∀α. Identity α → f α. Taka returnjest transformacja Identity → f.

Teraz możemy myśleć o monadzie jako o algebrze opartej na funktorze fz operacjami f ∘ f → fi Identity → f. Czy to nie wygląda znajomo? Jest bardzo podobny do monoidu, który był po prostu jakimś rodzajem τoperacji τ × τ → τi () → τ.

Więc monada jest jak monoid, tyle że zamiast typu mamy funktor. To ten sam rodzaj algebry, tylko w innej kategorii. (Z tego, co wiem, wyrażenie „monada jest po prostu monoidą w kategorii endofunkcji”).

Teraz mamy te dwie operacje: f ∘ f → fi Identity → f. Aby uzyskać odpowiednią węgielnicę, po prostu odwracamy strzałki. To daje nam dwie nowe operacje: f → f ∘ fi f → Identity. Możemy zamienić je na typy Haskella, dodając zmienne typu jak wyżej, dając nam ∀α. f α → f (f α)i ∀α. f α → α. Wygląda to tak jak definicja comonad:

class Functor f ⇒ Comonad f where
  coreturn ∷ f α → α
  cojoin   ∷ f α → f (f α)

Więc comonad jest wtedy coalgebra w kategorii endofunctors.

Algebry F i algebry F są strukturami matematycznymi, które odgrywają kluczową rolę w rozumowaniu typów indukcyjnych (lub typów rekurencyjnych ).

Algebry F.

Zaczniemy od algebry F. Spróbuję być tak prosty, jak to możliwe.

Chyba wiesz, co to jest typ rekurencyjny. Na przykład jest to typ listy liczb całkowitych:

data IntList = Nil | Cons (Int, IntList)

Oczywiste jest, że jest rekurencyjne - w rzeczywistości jego definicja odnosi się do samego siebie. Jego definicja składa się z dwóch konstruktorów danych, które mają następujące typy:

Nil  :: () -> IntList
Cons :: (Int, IntList) -> IntList

Zauważ, że napisałem typ Niljako () -> IntList, a nie po prostu IntList. Są to w rzeczywistości typy równoważne z teoretycznego punktu widzenia, ponieważ ()typ ma tylko jednego mieszkańca.

Jeśli napiszemy podpisy tych funkcji w bardziej teoretyczny sposób, otrzymamy

Nil  :: 1 -> IntList
Cons :: Int × IntList -> IntList

gdzie 1jest zestaw jednostek (zestaw z jednym elementem), a A × Boperacja jest iloczynem krzyżowym dwóch zestawów Ai B(to znaczy zestawu par, w (a, b)którym aprzechodzą wszystkie elementy Ai bprzechodzą przez wszystkie elementy B).

Rozłączne połączenie dwóch zbiorów Ai Bjest zbiorem A | Bbędącym połączeniem zbiorów {(a, 1) : a in A}i {(b, 2) : b in B}. Zasadniczo jest to zestaw wszystkich elementów z obu Ai B, ale z każdym z tych elementów „oznaczonymi” jako należącymi do jednego Alub jednego z nich B, więc kiedy wybieramy dowolny element z A | B, od razu będziemy wiedzieć, czy ten element pochodzi Aczy z B.

Możemy „połączyć” Nili Consfunkcje, aby utworzyły jedną funkcję działającą na zestawie 1 | (Int × IntList):

Nil|Cons :: 1 | (Int × IntList) -> IntList

Rzeczywiście, jeśli Nil|Consfunkcja jest zastosowana do ()wartości (która oczywiście należy do 1 | (Int × IntList)zestawu), zachowuje się tak, jakby była Nil; jeśli Nil|Consjest zastosowany do dowolnej wartości typu (Int, IntList)(takie wartości są również w zestawie 1 | (Int × IntList), zachowuje się jak Cons.

Teraz rozważ inny typ danych:

data IntTree = Leaf Int | Branch (IntTree, IntTree)

Ma następujące konstruktory:

Leaf   :: Int -> IntTree
Branch :: (IntTree, IntTree) -> IntTree

które można również połączyć w jedną funkcję:

Leaf|Branch :: Int | (IntTree × IntTree) -> IntTree

Można zauważyć, że obie te joinedfunkcje mają podobny typ: oba wyglądają

f :: F T -> T

gdzie Fjest rodzajem transformacji, która trwa nasz typ i daje bardziej złożony typ, który składa się xi |operacje, zwyczajów Ti ewentualnie inne typy. Na przykład dla IntListi IntTree Fwygląda następująco:

F1 T = 1 | (Int × T)
F2 T = Int | (T × T)

Od razu możemy zauważyć, że każdy typ algebraiczny można zapisać w ten sposób. Rzeczywiście dlatego nazywane są „algebraicznymi”: składają się z szeregu „sum” (związków) i „produktów” (produktów krzyżowych) innych typów.

Teraz możemy zdefiniować algebrę F. Algebra F to tylko para (T, f), gdzie Tjest jakiś typ i fjest funkcją typu f :: F T -> T. W naszych przykładach F-algebrami są (IntList, Nil|Cons)i (IntTree, Leaf|Branch). Zauważ jednak, że pomimo tego typu ffunkcji jest taki sam dla każdego F Ti fsame mogą być dowolne. Na przykład (String, g :: 1 | (Int x String) -> String)lub (Double, h :: Int | (Double, Double) -> Double)dla niektórych gi hsą również algebrami F dla odpowiednich F.

Następnie możemy wprowadzić homomorfizmy algebry F, a następnie początkowe algebry F , które mają bardzo przydatne właściwości. W rzeczywistości (IntList, Nil|Cons)jest to początkowa algebra F1 i (IntTree, Leaf|Branch)jest to początkowa algebra F2. Nie przedstawię dokładnych definicji tych terminów i właściwości, ponieważ są one bardziej złożone i abstrakcyjne niż jest to konieczne.

Niemniej fakt, że powiedzmy, (IntList, Nil|Cons)jest algebrą F, pozwala nam zdefiniować foldfunkcję podobną do tego typu. Jak wiadomo, fold jest rodzajem operacji, która przekształca niektóre rekurencyjne typy danych w jedną skończoną wartość. Na przykład możemy złożyć listę liczb całkowitych w jedną wartość, która jest sumą wszystkich elementów na liście:

foldr (+) 0 [1, 2, 3, 4] -> 1 + 2 + 3 + 4 = 10

Możliwe jest uogólnienie takiej operacji na dowolnym rekurencyjnym typie danych.

Poniżej znajduje się podpis foldrfunkcji:

foldr :: ((a -> b -> b), b) -> [a] -> b

Zauważ, że użyłem nawiasów klamrowych do oddzielenia dwóch pierwszych argumentów od ostatniego. To nie jest prawdziwa foldrfunkcja, ale jest z nią izomorficzna (to znaczy, możesz łatwo uzyskać jedną od drugiej i odwrotnie). Częściowo zastosowany foldrbędzie miał następujący podpis:

foldr ((+), 0) :: [Int] -> Int

Widzimy, że jest to funkcja, która pobiera listę liczb całkowitych i zwraca jedną liczbę całkowitą. Zdefiniujmy taką funkcję w kategoriach naszego IntListtypu.

sumFold :: IntList -> Int
sumFold Nil         = 0
sumFold (Cons x xs) = x + sumFold xs

Widzimy, że ta funkcja składa się z dwóch części: pierwsza część określa zachowanie tej funkcji po Nilczęści IntList, a druga część określa zachowanie funkcji po Consczęści.

Załóżmy teraz, że programujemy nie w języku Haskell, ale w jakimś języku, który pozwala na użycie typów algebraicznych bezpośrednio w podpisach typów (cóż, technicznie Haskell pozwala na użycie typów algebraicznych przez krotki i Either a btypy danych, ale doprowadzi to do niepotrzebnej gadatliwości). Rozważ funkcję:

reductor :: () | (Int × Int) -> Int
reductor ()     = 0
reductor (x, s) = x + s

Można zauważyć, że reductorjest to funkcja typu F1 Int -> Int, podobnie jak w definicji F-algebry! Rzeczywiście, para (Int, reductor)jest algebrą F1.

Ponieważ IntListjest to początkowa algebra F1, dla każdego typu Ti dla każdej funkcji r :: F1 T -> Tistnieje funkcja, zwana katamorfizmem, dla rktórej konwertuje IntListsię Ti taka funkcja jest unikalna. Rzeczywiście, w naszym przykładzie catamorphism za reductorto sumFold. Uwaga, jak reductori sumFoldsą podobne: mają prawie taką samą strukturę! W reductordefinicji sużycie parametru (którego typ odpowiada T) odpowiada wykorzystaniu wyniku obliczenia sumFold xsw sumFolddefinicji.

Żeby było jaśniej i pomóc zobaczyć wzór, oto kolejny przykład, a my znów zaczniemy od wynikowej funkcji składania. Rozważ appendfunkcję, która dołącza swój pierwszy argument do drugiego:

(append [4, 5, 6]) [1, 2, 3] = (foldr (:) [4, 5, 6]) [1, 2, 3] -> [1, 2, 3, 4, 5, 6]

Tak to wygląda na naszych IntList:

appendFold :: IntList -> IntList -> IntList
appendFold ys ()          = ys
appendFold ys (Cons x xs) = x : appendFold ys xs

Ponownie spróbujmy napisać reduktor:

appendReductor :: IntList -> () | (Int × IntList) -> IntList
appendReductor ys ()      = ys
appendReductor ys (x, rs) = x : rs

appendFoldto katamorfizm, w appendReductorktóry przemienia IntListsię IntList.

Zasadniczo algebry F pozwalają nam definiować „fałdy” rekurencyjnych struktur danych, to znaczy operacje, które redukują nasze struktury do pewnej wartości.

F-carbongebras

Węglowodory F to tak zwane „dualne” określenie dla algebr F. Pozwalają nam zdefiniować unfoldsrekurencyjne typy danych, czyli sposób konstruowania struktur rekurencyjnych z pewnej wartości.

Załóżmy, że masz następujący typ:

data IntStream = Cons (Int, IntStream)

To jest nieskończony strumień liczb całkowitych. Jego jedyny konstruktor ma następujący typ:

Cons :: (Int, IntStream) -> IntStream

Lub pod względem zestawów

Cons :: Int × IntStream -> IntStream

Haskell pozwala na dopasowanie wzorca do konstruktorów danych, dzięki czemu można zdefiniować następujące funkcje działające na IntStreams:

head :: IntStream -> Int
head (Cons (x, xs)) = x

tail :: IntStream -> IntStream
tail (Cons (x, xs)) = xs

Możesz oczywiście łączyć te funkcje w jedną funkcję typu IntStream -> Int × IntStream:

head&tail :: IntStream -> Int × IntStream
head&tail (Cons (x, xs)) = (x, xs)

Zauważ, że wynik funkcji pokrywa się z algebraiczną reprezentacją naszego IntStreamtypu. Podobnie można zrobić w przypadku innych typów danych rekurencyjnych. Być może już zauważyłeś wzór. Mam na myśli rodzinę funkcji typu

g :: T -> F T

gdzie Tjest jakiś typ. Od teraz będziemy definiować

F1 T = Int × T

Teraz F-węgielgebra jest parą (T, g), w której Tjest typem i gjest funkcją typu g :: T -> F T. Na przykład (IntStream, head&tail)jest węgiel F1. Ponownie, podobnie jak w F-algebrach, gi Tmoże być dowolne, na przykład, (String, h :: String -> Int x String)jest także węglową F1 przez jakiś czas.

Wśród wszystkich F-węgli F są takie tak zwane F-węgiel F terminali , które są dualne do początkowych F-algeb. Na przykład IntStreamjest terminalem F-carbongebra. Oznacza to, że dla każdego typu Ti dla każdej funkcji p :: T -> F1 Tistnieje funkcja zwana anamorfizmem , która przekształca Tsię IntStreami taka funkcja jest unikalna.

Rozważ następującą funkcję, która generuje strumień kolejnych liczb całkowitych, zaczynając od podanej:

nats :: Int -> IntStream
nats n = Cons (n, nats (n+1))

Teraz sprawdźmy funkcję natsBuilder :: Int -> F1 Int, to znaczy natsBuilder :: Int -> Int × Int:

natsBuilder :: Int -> Int × Int
natsBuilder n = (n, n+1)

Ponownie widzimy pewne podobieństwo między natsi natsBuilder. Jest bardzo podobny do połączenia, które zaobserwowaliśmy wcześniej z reduktorami i fałdami. natsjest anamorfizmem dla natsBuilder.

Kolejny przykład: funkcja, która przyjmuje wartość i funkcję i zwraca strumień kolejnych zastosowań funkcji do wartości:

iterate :: (Int -> Int) -> Int -> IntStream
iterate f n = Cons (n, iterate f (f n))

Jego funkcja konstruktora jest następująca:

iterateBuilder :: (Int -> Int) -> Int -> Int × Int
iterateBuilder f n = (n, f n)

Potem iteratejest anamorfizm iterateBuilder.

Wniosek

Krótko mówiąc, algebry F pozwalają definiować fałdy, to znaczy operacje, które redukują strukturę rekurencyjną do jednej wartości, a algebry F pozwalają robić coś przeciwnego: konstruować [potencjalnie] nieskończoną strukturę z jednej wartości.

W rzeczywistości w Haskell F-algebry i F-carbongebras pokrywają się. Jest to bardzo przyjemna właściwość, która jest konsekwencją obecności „dolnej” wartości w każdym typie. Tak więc w Haskell można tworzyć i rozkładać dla każdego typu rekurencyjnego. Jednak model teoretyczny stojący za tym jest bardziej złożony niż ten, który przedstawiłem powyżej, więc celowo tego uniknąłem.

Mam nadzieję że to pomoże.

Przegląd artykułu z samouczka Samouczek dotyczący (ko) algeb i indukcji (co) powinien dać ci wgląd w koalgebrę w informatyce.

Oto cytat z tego, aby Cię przekonać,

Ogólnie rzecz biorąc, program w pewnym języku programowania manipuluje danymi. Podczas rozwoju informatyki w ciągu ostatnich kilku dziesięcioleci stało się jasne, że pożądany jest abstrakcyjny opis tych danych, na przykład w celu upewnienia się, że program nie zależy od szczególnego przedstawienia danych, na których działa. Taka abstrakcja ułatwia także sprawdzenie poprawności.
Pragnienie to doprowadziło do zastosowania metod algebraicznych w informatyce, w gałęzi zwanej specyfikacją algebraiczną lub abstrakcyjną teorią typów danych. Przedmiotem badań są same w sobie typy danych, wykorzystujące pojęcia technik znanych z algebry. Typy danych używane przez informatyków są często generowane z danego zbioru operacji (konstruktorów) iz tego powodu „inicjał” algebry odgrywa tak ważną rolę.
Standardowe techniki algebraiczne okazały się przydatne do uchwycenia różnych istotnych aspektów struktur danych wykorzystywanych w informatyce. Okazało się jednak, że algebraicznie trudno jest opisać niektóre z natury dynamiczne struktury występujące w informatyce. Takie struktury zwykle obejmują pojęcie państwa, które można przekształcić na różne sposoby. Formalne podejścia do takich opartych na stanach układów dynamicznych zwykle wykorzystują automaty lub układy przejściowe, jako klasyczne wczesne odniesienia.
W ciągu ostatniej dekady stopniowo narastał pogląd, że takie systemy oparte na stanie nie powinny być opisywane jako algebry, ale jako tak zwane koalgebry. Są to formalne podwójne algebry, w sposób, który zostanie sprecyzowany w tym samouczku. Podwójna właściwość „początkowości” algebry, a mianowicie ostateczność, okazała się kluczowa dla takich algebr. A logiczną zasadą rozumowania potrzebną do takich ostatecznych koalergii nie jest indukcja, ale koindukcja.

Preludium na temat teorii kategorii. Teorią kategorii powinna być nazwa teorii funktorów. Ponieważ kategorie są tym, co należy zdefiniować, aby zdefiniować funktory. (Ponadto funktory są tym, co należy zdefiniować, aby zdefiniować naturalne przekształcenia).

Co to jest funktor? Jest to transformacja z jednego zestawu do drugiego, który zachowuje ich strukturę. (Aby uzyskać więcej szczegółów, w sieci jest wiele dobrych opisów).

Co to jest algebra F. To algebra funktora. To tylko badanie uniwersalnej właściwości funktora.

Jak można to powiązać z informatyką? Program może być postrzegany jako uporządkowany zestaw informacji. Wykonanie programu odpowiada modyfikacji tego uporządkowanego zestawu informacji. Brzmi dobrze, że wykonanie powinno zachować strukturę programu. Następnie wykonanie można uznać za zastosowanie funktora w stosunku do tego zestawu informacji. (Ten, który definiuje program).

Dlaczego F-co-algebra? Programy są w istocie dualne, ponieważ są opisywane przez informacje i działają na ich podstawie. Wtedy głównie informacje, które składają się na program i powodują ich zmianę, można wyświetlić na dwa sposoby.

• Dane, które można zdefiniować jako informacje przetwarzane przez program.
• Stan, który można zdefiniować jako informację udostępnianą przez program.

Na tym etapie chciałbym powiedzieć,

• Algebra F to badanie transformacji funkcjonalnej działającej na Wszechświat Danych (jak zdefiniowano tutaj).
• F-algebry to badanie transformacji funkcjonalnej działającej na Wszechświat Stanu (jak tutaj zdefiniowano).

W trakcie trwania programu dane i państwo współistnieją i się uzupełniają. Są podwójne.

Zacznę od rzeczy, które są oczywiście związane z programowaniem, a następnie dodam matematykę, aby zachować ją tak konkretną i praktyczną, jak to tylko możliwe.

Przytoczmy kilku informatyków o koindukcji…

http://www.cs.umd.edu/~micinski/posts/2012-09-04-on-understanding-coinduction.html

Indukcja dotyczy danych skończonych, koindukcja dotyczy danych nieskończonych.

Typowym przykładem nieskończonych danych jest typ leniwej listy (strumień). Załóżmy na przykład, że mamy w pamięci następujący obiekt:

 let (pi : int list) = (* some function which computes the digits of
 π. *)

Komputer nie może pomieścić całego π, ponieważ ma tylko skończoną ilość pamięci! Ale to, co może zrobić, to mieć skończony program, który wytworzy dowolne długie rozszerzenie π, jakiego sobie życzysz. Tak długo, jak używasz tylko skończonych elementów listy, możesz obliczyć na tej nieskończonej liście tyle, ile potrzebujesz.

Rozważ jednak następujący program:

let print_third_element (k : int list) =   match k with
     | _ :: _ :: thd :: tl -> print thd


 print_third_element pi

Ten program powinien wydrukować trzecią cyfrę pi. Ale w niektórych językach każdy argument funkcji jest oceniany przed przekazaniem do funkcji (ścisła, nie leniwa ocena). Jeśli użyjemy tego polecenia redukcji, nasz powyższy program będzie działał na zawsze, obliczając cyfry pi, zanim będzie mógł zostać przekazany do naszej funkcji drukarki (co nigdy się nie zdarza). Ponieważ maszyna nie ma nieskończonej pamięci, programowi ostatecznie zabraknie pamięci i ulegnie awarii. To może nie być najlepsza kolejność oceny.

http://adam.chlipala.net/cpdt/html/Coinductive.html

W leniwych funkcjonalnych językach programowania, takich jak Haskell, nieskończone struktury danych są wszędzie. Nieskończone listy i bardziej egzotyczne typy danych zapewniają wygodne abstrakty do komunikacji między częściami programu. Osiągnięcie podobnej wygody bez nieskończonych leniwych struktur wymagałoby w wielu przypadkach akrobatycznego odwrócenia przepływu sterowania.

http://www.alexandrasilva.org/#/talks.html

Powiązanie kontekstu matematycznego z otoczeniem ze zwykłymi zadaniami programistycznymi

Co to jest „algebra”?

Struktury algebraiczne ogólnie wyglądają następująco:

1. Rzeczy
2. Co mogą zrobić

Powinno to brzmieć jak obiekty z 1. właściwościami i 2. metodami. Lub jeszcze lepiej, powinno to brzmieć jak podpisy tekstowe.

Standardowe przykłady matematyczne obejmują monoid ⊃ grupę ⊃ przestrzeń wektorową ⊃ „algebrę”. Monoidy są jak automaty: sekwencje czasowników (np f.g.h.h.nothing.f.g.f.). gitDziennika, który zawsze dodaje historii i nigdy nie usuwa to byłoby monoid ale nie grupa. Jeśli dodasz odwrotność (np. Liczby ujemne, ułamki, pierwiastki, usunięcie nagromadzonej historii, nie rozbicie zepsutego lustra), otrzymasz grupę.

Grupy zawierają elementy, które można dodawać lub odejmować razem. Na przykład Durationmożna dodać razem. (Ale Dates nie może.) Czasy trwają w przestrzeni wektorowej (nie tylko w grupie), ponieważ można je również skalować według liczb zewnętrznych. (Podpis typu scaling :: (Number,Duration) → Duration.)

Algebry - przestrzenie wektorowe mogą zrobić jeszcze jedną rzecz: jest kilka m :: (T,T) → T. Nazwij to „mnożeniem” lub nie, ponieważ kiedy wyjdziesz Integers, mniej oczywiste powinno być „mnożenie” (lub „potęgowanie” ).

(Jest to dlaczego ludzie patrzą na () Właściwości uniwersalnych kategorii-teoretyczna: im powiedzieć, co mnożenie powinno robić lub być jak :

)

Algebras → Coalgebras

Kombinacja jest łatwiejsza do zdefiniowania w sposób, który wydaje się nieobowiązkowy, niż multiplikacja, ponieważ aby wyjść T → (T,T), możesz po prostu powtórzyć ten sam element. („mapa diagonalna” - podobnie jak diagonalne macierze / operatory w teorii spektralnej)

Rzeczownik jest zwykle śladem (sumą przekątnych wpisów), chociaż znowu ważne jest to, co robi Twój rzecz ; tracejest po prostu dobrą odpowiedzią na macierze.

Powodem, dla którego warto spojrzeć na podwójną przestrzeń , jest to, że łatwiej jest w niej myśleć. Na przykład czasem łatwiej jest pomyśleć o normalnym wektorze niż o płaszczyźnie, do której jest normalny, ale można kontrolować płaszczyzny (w tym hiperpłaszczyzny) za pomocą wektorów (a teraz mówię o znanym wektorze geometrycznym, jak w przypadku promienia świetlnego) .

Oswajanie (nie) ustrukturyzowanych danych

Matematycy mogą modelować coś zabawnego jak TQFT , podczas gdy programiści muszą się zmagać

• daty / godziny ( + :: (Date,Duration) → Date),
• miejsca ( Paris≠ (+48.8567,+2.3508)! To kształt, nie punkt.),
• nieustrukturyzowany JSON, który w pewnym sensie powinien być spójny,
• źle-ale-zamknij XML,
• niezwykle złożone dane GIS, które powinny zaspokoić mnóstwo rozsądnych relacji,
• wyrażenia regularne, które coś dla ciebie znaczyły , ale znacznie mniej znaczy perl.
• CRM, który powinien przechowywać wszystkie numery telefonów kierownika i lokalizacje willi, nazwiska jego (obecnie byłej) żony i dzieci, urodziny i wszystkie poprzednie prezenty, z których każdy powinien spełniać „oczywiste” relacje (oczywiste dla klienta), które są niewiarygodnie trudne do zakodowania,
• .....

Informatycy, mówiąc o węgielnicach, zwykle mają na myśli ustalone operacje, takie jak produkt kartezjański. Wierzę, że to właśnie ludzie mają na myśli, mówiąc: „Algebry są węgielnicami w Haskell”. Ale w takim stopniu, w jakim programiści muszą modelować złożone typy danych, takie jak Place, Date/Timei Customer- i sprawić, aby modele te wyglądały tak bardzo jak świat rzeczywisty (lub przynajmniej widok rzeczywistego świata użytkownika końcowego) - uważam, że dualistyczne, może być użyteczne poza światem zestalonym.