Haskell Language
Teoria kategorii

Teoria kategorii jako system organizacji abstrakcji

Teoria kategorii jest nowoczesną teorią matematyczną i gałęzią algebry abstrakcyjnej skupioną na naturze powiązań i relacji. Jest przydatny do tworzenia solidnych podstaw i wspólnego języka dla wielu abstrakcji programowych wielokrotnego użytku. Haskell wykorzystuje teorię kategorii jako inspirację dla niektórych podstawowych typów dostępnych zarówno w bibliotece standardowej, jak i kilku popularnych bibliotekach stron trzecich.

Przykład

Functor typeclass mówi, że jeśli typ F wystąpienie Functor (dla których piszemy Functor F ), wówczas mamy ogólny operację

fmap :: (a -> b) -> (F a -> F b)

co pozwala nam „mapować” na F Średnia (ale niedoskonały) intuicja jest taka, że F a to pojemnik pełen wartości typu a i fmap pozwala nam zastosować transformację do każdego z tych elementów zawartych. Przykładem jest Maybe

instance Functor Maybe where
  fmap f Nothing = Nothing     -- if there are no values contained, do nothing
  fmap f (Just a) = Just (f a) -- else, apply our transformation

Biorąc pod uwagę tę intuicję, powszechne pytanie brzmi: „dlaczego nie nazwać Functor czymś oczywistym, takim jak Mappable ?”.

Podpowiedź teorii kategorii

Powodem jest to, że Functor wpasowuje się w zbiór wspólnych struktur w teorii kategorii, a zatem nazywając Functor „Functor”, możemy zobaczyć, jak łączy się z tym głębszym zasobem wiedzy.

W szczególności teoria kategorii jest bardzo zainteresowana ideą strzałek z jednego miejsca do drugiego. W Haskell najważniejszym zestawem strzałek są strzałki funkcyjne a -> b . Wspólną rzeczą do studiowania w teorii kategorii jest to, w jaki sposób jeden zestaw strzałek odnosi się do innego zestawu. W szczególności, dla każdego typu konstruktora F , interesujący jest także zestaw strzałek o kształcie F a -> F b .

Więc jest jakiś funktor F taki, że istnieje związek między normalnym Haskell strzałki a -> b i F strzały specyficznych dla F a -> F b . Połączenie jest zdefiniowane przez fmap i rozpoznajemy również kilka praw, które muszą obowiązywać

forall (x :: F a) . fmap id x == x

forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)

Wszystkie te prawa wynikają naturalnie z teoretycznej interpretacji Functor i nie byłyby tak oczywiście konieczne, gdybyśmy pomyśleli o Functor jako odnoszącym się do „mapowania elementów”.

Definicja kategorii

Kategoria C obejmuje:

• Zbiór obiektów o nazwie Obj(C) ;
• Zbiór (zwany Hom(C) ) morfizmów między tymi obiektami. Jeśli i a b są Obj(C) , a następnie morfizmem f w Hom(C) jest zwykle oznaczony f : a -> b i zbierania wszystkich morfizmu pomiędzy i a b jest oznaczona hom(a,b) ;
• Specjalny morfizm zwany morfizmem tożsamości - dla każdego a : Obj(C) istnieje id : a -> a morfizmu id : a -> a ;
• Operator kompozycji ( . ), Przyjmujący dwa morfizmy f : a -> b , g : b -> c i wytwarzający morfizm a -> c

które przestrzegają następujących praw:

For all f : a -> x, g : x -> b, then id . f = f and g . id = g

For all f : a -> b, g : b -> c and h : c -> d, then h . (g . f) = (h . g) . f

Innymi słowy, kompozycja z morfizmem tożsamości (po lewej lub po prawej) nie zmienia drugiego morfizmu, a kompozycja jest asocjacyjna.

W Haskell Category jest zdefiniowana jako typ w Control.Category :

-- | A class for categories.
--   id and (.) must form a monoid.
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

W tym przypadku cat :: k -> k -> * obiektywizuje relację morfizmu - istnieje morfizm cat ab wtedy i tylko wtedy, gdy cat ab jest zamieszkały (tj. Ma wartość). , b i c są w Obj(C) . Sam Obj(C) jest reprezentowany przez rodzaj k - na przykład, gdy k ~ * , jak to zwykle bywa, obiekty są typami.

Kanonicznym przykładem kategorii w Haskell jest kategoria funkcji:

instance Category (->) where
  id = Prelude.id
  (.) = Prelude..

Innym typowym przykładem jest Category z Kleisli strzałki dla Monad :

newtype Kleisli m a b = Kleisli (a -> m b)

class Monad m => Category (Kleisli m) where
  id = Kleisli return
  Kleisli f . Kleisli g = Kleisli (f >=> g)

Typy Haskella jako kategorię

Definicja kategorii

Typy Haskella wraz z funkcjami między typami tworzą (prawie †) kategorię. Mamy morfizm tożsamości (funkcję) ( id :: a -> a ) dla każdego obiektu (typu) a ; i skład morfizmów ( (.) :: (b -> c) -> (a -> b) -> a -> c ), które spełniają prawa kategorii:

f . id = f = id . f
h . (g . f) = (h . g) . f 

Zwykle nazywamy tę kategorię Hask .

Izomorfizmy

W teorii kategorii mamy izomorfizm, gdy mamy morfizm, który ma odwrotność, innymi słowy, istnieje morfizm, który można z nim skomponować w celu stworzenia tożsamości. W Hask oznacza to parę morfizmów f , g takich, że:

 f . g == id == g . f

Jeśli znajdziemy parę takich morfizmów między dwoma typami, nazywamy je izomorficzne względem siebie .

Przykładem dwóch typów izomorficznych byłoby ((),a) i a dla niektórych a . Możemy zbudować dwa morfizmy:

f :: ((),a) -> a
f ((),x) = x

g :: a -> ((),a)
g x = ((),x)

I możemy to sprawdzić f . g == id == g . f .

Functors

Funktor w teorii kategorii przechodzi z jednej kategorii do drugiej, mapując obiekty i morfizmy. Pracujemy tylko nad jedną kategorią, kategorią Hask typów Haskell, więc zobaczymy tylko funktory od Hask do Hask , te funktory, których kategoria pochodzenia i przeznaczenia są takie same, nazywane są endofunkcjami . Nasi endofunktorzy będą typami polimorficznymi przyjmującymi typ i zwracającymi inny:

F :: * -> *

Przestrzeganie kategorycznych praw funktorów (zachowanie tożsamości i składu) jest równoznaczne z przestrzeganiem praw funktorów Haskella:

fmap (f . g) = (fmap f) . (fmap g)
fmap id = id

Mamy na przykład, że [] , Maybe lub (-> r) są funktorami w Hask .

Monady

Monada w teorii kategorii jest monoidą w kategorii endofunkorów . Ta kategoria ma endofunkcje jako obiekty F :: * -> * i transformacje naturalne (transformacje między nimi dla wszystkich forall a . F a -> G a ) jako morfizmy.

Obiekt monoidalny można zdefiniować w kategorii monoidalnej i jest on typem mającym dwa morfizmy:

zero :: () -> M
mappend :: (M,M) -> M

Możemy to z grubsza przetłumaczyć na kategorię endofunkorów Hask jako:

return :: a -> m a
join :: m (m a) -> m a 

I przestrzeganie praw monady jest równoznaczne z przestrzeganiem kategorycznych praw dotyczących obiektów monoidów.

† W rzeczywistości klasa wszystkich typów wraz z klasą funkcji między typami nie tworzą ściśle kategorii w Haskell, z powodu istnienia undefined . Zazwyczaj można temu zaradzić, po prostu definiując obiekty kategorii Hask jako typy bez wartości dolnych, co wyklucza funkcje nie kończące się i wartości nieskończone (kodaty). Szczegółowe omówienie tego tematu znajduje się tutaj .

Produkt typów w Hask

Produkty kategoryczne

W teorii kategorii iloczyn dwóch obiektów X , Y jest innym obiektem Z o dwóch rzutach: π₁: Z → X i π₂: Z → Y ; tak, że wszelkie pozostałe dwa morfizmy z innego obiektu rozkładają się jednoznacznie poprzez te projekcje. Innymi słowy, jeśli istnieją f₁: W → X i f₂: W → Y , istnieje unikalny morfizm g: W → Z taki, że π₁ ○ g = f₁ i π₂ ○ g = f₂ .

Produkty w Hask

Przekłada się to na następującą kategorię Hask typów Haskell, Z jest iloczynem A , B gdy:

-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g  :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2

Rodzaj produktu dwóch typów A , B , który jest zgodny z powyższym prawem, to krotka dwóch typów (A,B) , a dwa występy to fst i snd . Możemy sprawdzić, czy przestrzega powyższej zasady, jeśli mamy dwie funkcje f1 :: W -> A i f2 :: W -> B , możemy je jednoznacznie rozłożyć w następujący sposób:

decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))

I możemy sprawdzić, czy rozkład jest prawidłowy:

fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2

Wyjątkowość aż do izomorfizmu

Wybór (A,B) jako produktu A i B nie jest wyjątkowy. Innym logicznym i równoważnym wyborem byłby:

data Pair a b = Pair a b

Co więcej, moglibyśmy również wybrać (B,A) jako produkt, a nawet (B,A,()) , i moglibyśmy znaleźć funkcję rozkładu podobną do powyższej, również zgodnie z następującymi zasadami:

decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))

Wynika to z faktu, że produkt nie jest wyjątkowy, ale wyjątkowy aż do izomorfizmu . Co dwa produkty A i B nie muszą być równe, ale powinny być izomorficzne. Na przykład dwa zdefiniowane przez nas różne produkty (A,B) i (B,A,()) są izomorficzne:

iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())

iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)

Niepowtarzalność rozkładu

Należy zauważyć, że również funkcja rozkładu musi być unikalna. Istnieją typy, które spełniają wszystkie zasady wymagane dla produktu, ale rozkład nie jest unikalny. Jako przykład możemy spróbować użyć (A,(B,Bool)) z rzutami fst fst . snd jako produkt A i B :

decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))

Możemy sprawdzić, czy to działa:

fst         . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x

Problem polega jednak na tym, że mogliśmy napisać kolejny rozkład, a mianowicie:

decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))

A ponieważ rozkład nie jest unikalny , (A,(B,Bool)) nie jest produktem A i B w Hask

Koprodukt typów w Hask

Intuicja

Kategoryczny produkt dwóch typów A i B powinien zawierać minimalną ilość informacji koniecznych do umieszczenia w wystąpieniu typu A lub typu B. Widzimy teraz, że intuicyjnym koproduktem dwóch typów powinien być Either ab . Inni kandydaci, na przykład Either a (b,Bool) , będą zawierać część niepotrzebnych informacji i nie będą minimalne.

Formalna definicja pochodzi od kategorycznej definicji koproduktu.

Kategoryczne produkty uboczne

Kategoryczny produkt uboczny to podwójne pojęcie produktu kategorycznego. Uzyskuje się to bezpośrednio poprzez odwrócenie wszystkich strzałek w definicji produktu. Koprodukt dwóch obiektów X , Y to kolejny obiekt Z z dwoma inkluzjami: i_1: X → Z oraz i_2: Y → Z ; tak, że wszelkie pozostałe dwa morfizmy od X i Y do innego obiektu rozkładają się jednoznacznie poprzez te wtrącenia. Innymi słowy, jeśli istnieją dwa morfizmy f₁: X → W i f₂: Y → W , istnieje unikalny morfizm g: Z → W taki, że g ○ i₁ = f₁ i g ○ i₂ = f₂

Koprodukty w Hask

Tłumaczenie na kategorię Hask jest podobne do tłumaczenia produktu:

-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g  :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2

Koproduktem dwóch typów A i B w Hask jest Either ab lub inny typ izomorficzny:

-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b

-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x)  = f1 x
decompose f1 f2 (Right y) = f2 y 

Aplikacja Haskell pod względem teorii kategorii

Functor Haskella pozwala na mapowanie dowolnego typu a (obiekt Hask ) na typ F a a także mapowanie funkcji a -> b (morfizm Hask ) na funkcję typu F a -> F b . Odpowiada to definicji teorii kategorii w tym sensie, że funktor zachowuje podstawową strukturę kategorii.

Kategoria monoidalna to kategoria o pewnej dodatkowej strukturze:

• Produkt tensorowy (patrz Produkt typów w Hask )
• Jednostka tensorowa (obiekt jednostkowy)

Biorąc parę za nasz produkt, tę definicję można przetłumaczyć na Haskell w następujący sposób:

class Functor f => Monoidal f where
    mcat :: f a -> f b -> f (a,b)
    munit :: f ()

Klasa Applicative jest odpowiednikiem tej Monoidal i dlatego może być zaimplementowana pod względem:

instance Monoidal f => Applicative f where
    pure x = fmap (const x) munit
    f <*> fa = (\(f, a) -> f a) <$> (mcat f fa)