Haskell Language
Categorie theorie

Categorie theorie als een systeem voor het organiseren van abstractie

Categorie theorie is een moderne wiskundige theorie en een tak van abstracte algebra gericht op de aard van verbondenheid en relatie. Het is nuttig voor het leggen van een solide basis en gemeenschappelijke taal voor veel zeer herbruikbare programmeerabstracties. Haskell gebruikt de categorietheorie als inspiratie voor enkele van de kerntypeklassen die beschikbaar zijn in zowel de standaardbibliotheek als verschillende populaire externe bibliotheken.

Een voorbeeld

De Functor typeclass zegt dat als een type F Functor instantieert (waarvoor we Functor F schrijven), we een generieke bewerking hebben

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

waarmee we over F kunnen 'mappen'. De standaard (maar imperfecte) intuïtie is dat F a container is met waarden van type a en met fmap kunnen we een transformatie toepassen op elk van deze elementen. Een voorbeeld is 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

Gegeven deze intuïtie is een veel voorkomende vraag "waarom Functor zo voor de hand liggend als Mappable ?".

Een hint van categorietheorie

De reden is dat Functor in een reeks gemeenschappelijke structuren in de categorietheorie past en daarom door Functor "Functor" te noemen, kunnen we zien hoe het aansluit op dit diepere geheel van kennis.

In het bijzonder houdt Category Theory zich sterk bezig met het idee van pijlen van de ene plaats naar de andere. In Haskell zijn de belangrijkste pijlen de functiepijlen a -> b . Het is gebruikelijk om in Categorie Theorie te bestuderen hoe de ene set pijlen zich verhoudt tot een andere set. In het bijzonder is voor elk type constructor F de reeks pijlen van de vorm F a -> F b ook interessant.

Een functor is dus elke F zodanig dat er een verband bestaat tussen normale Haskell-pijlen a -> b en de F specifieke pijlen F a -> F b . De verbinding wordt gedefinieerd door fmap en we erkennen ook enkele wetten die moeten gelden

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

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

Al deze wetten vloeien op natuurlijke wijze voort uit de Categorie Theoretische interpretatie van Functor en zouden niet zo vanzelfsprekend noodzakelijk zijn als we alleen aan Functor denken als betrekking hebbend op "mapping over elementen".

Definitie van een categorie

Een categorie C bestaat uit:

• Een verzameling objecten genaamd Obj(C) ;
• Een verzameling ( Hom(C) ) van morfismen tussen die objecten. Als a en b in Obj(C) , wordt een morfisme f in Hom(C) typisch aangeduid als f : a -> b , en wordt de verzameling van alle morfisme tussen a en b aangeduid als hom(a,b) ;
• Een speciaal morfisme genaamd identiteitsmorfisme - voor elke a : Obj(C) bestaat er een morfisme- id : a -> a ;
• Een compositie-operator ( . ), Neemt twee morfismen f : a -> b , g : b -> c en produceert een morfisme a -> c

die de volgende wetten naleven:

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

Met andere woorden, samenstelling met het identiteitsmorfisme (links of rechts) verandert niets aan het andere morfisme en de samenstelling is associatief.

In Haskell, de Category is gedefinieerd als een typeclass in 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

In dit geval maakt cat :: k -> k -> * de morfismerelatie objectief - er bestaat een morfisme cat ab als en alleen als cat ab bewoond is (dwz een waarde heeft). a , b en c staan allemaal in Obj(C) . Obj(C) zelf wordt vertegenwoordigd door het type k - bijvoorbeeld, wanneer k ~ * , zoals meestal het geval is, objecten zijn.

Het canonieke voorbeeld van een categorie in Haskell is de functiecategorie:

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

Een ander veel voorkomend voorbeeld is de Category Kleisli pijlen voor een 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)

Haskell-typen als een categorie

Definitie van de categorie

De Haskell-typen vormen samen met functies tussen typen (bijna †) een categorie. We hebben een identiteitsmorfisme (functie) ( id :: a -> a ) voor elk object (type) a ; en samenstelling van morfismen ( (.) :: (b -> c) -> (a -> b) -> a -> c ), die categoriewetten gehoorzamen:

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

We noemen deze categorie meestal Hask .

isomorfismen

In de categorietheorie hebben we een isomorfisme als we een morfisme hebben dat omgekeerd is, met andere woorden, er is een morfisme dat ermee kan worden samengesteld om de identiteit te creëren. In Hask komt dit neer op een paar morfismen f , g zodat:

 f . g == id == g . f

Als we een paar van dergelijke morfismen tussen twee typen vinden, noemen we ze isomorf voor elkaar .

Een voorbeeld van twee isomorfe typen is ((),a) en a voor sommige a . We kunnen de twee morfismen construeren:

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

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

En we kunnen controleren dat f . g == id == g . f .

functoren

Een functor, in de categorietheorie, gaat van een categorie naar een andere en brengt objecten en morfismen in kaart. We werken slechts aan één categorie, de categorie Hask van Haskell-typen, dus we gaan alleen functoren zien van Hask tot Hask , die functoren, waarvan de oorsprong en de bestemmingscategorie dezelfde zijn, worden endofunctors genoemd . Onze endofunctors zullen de polymorfe typen zijn die een type nemen en een ander retourneren:

F :: * -> *

Het gehoorzamen van de categorische functorwetten (behoud van identiteiten en samenstelling) is gelijk aan het gehoorzamen van de Haskell functorwetten:

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

Dus we hebben bijvoorbeeld dat [] , Maybe of (-> r) functors zijn in Hask .

monaden

Een monade in de categorietheorie is een monoïde op de categorie endofunctors . Deze categorie heeft endofunctors als objecten F :: * -> * en natuurlijke transformaties (transformaties daartussen voor forall a . F a -> G a Fa forall a . F a -> G a ) als morfismen.

Een monoid object kan worden gedefinieerd op een monoidal categorie en is een type met twee morfismen:

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

We kunnen dit grofweg vertalen naar de categorie Hask-endofunctors als:

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

En het gehoorzamen van de monadewetten is gelijk aan het gehoorzamen aan de categorische monoïde objectwetten.

† In feite vormt de klasse van alle typen samen met de klasse van functies tussen typen niet strikt een categorie in Haskell, vanwege het bestaan van undefined . Dit wordt meestal verholpen door eenvoudigweg de objecten van de Hask- categorie te definiëren als typen zonder bodemwaarden , waardoor niet-eindigende functies en oneindige waarden (codata) worden uitgesloten. Voor een gedetailleerde bespreking van dit onderwerp, zie hier .

Productsoort in Hask

Categorische producten

In de categorietheorie is het product van twee objecten X , Y een ander object Z met twee projecties: π₁: Z → X en π₂: Z → Y ; zodanig dat elke andere twee morfismen van een ander object op unieke wijze ontleden door die projecties. Met andere woorden, als er f₁: W → X en f₂: W → Y bestaat, bestaat er een uniek morfisme g: W → Z zodanig dat π₁ ○ g = f₁ en π₂ ○ g = f₂ .

Producten in Hask

Dit vertaalt zich als volgt in de Hask- categorie van Haskell-typen, Z is het product van A , B wanneer:

-- 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

Het producttype van twee typen A , B , die de hierboven genoemde wet volgt, is de tupel van de twee typen (A,B) , en de twee projecties zijn fst en snd . We kunnen controleren of het de bovenstaande regel volgt, als we twee functies f1 :: W -> A en f2 :: W -> B hebben, kunnen we ze als volgt uniek ontleden:

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

En we kunnen controleren of de ontleding correct is:

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

Uniek tot isomorfisme

De keuze van (A,B) als het product van A en B is niet uniek. Een andere logische en gelijkwaardige keuze zou zijn geweest:

data Pair a b = Pair a b

Bovendien hadden we ook (B,A) als product kunnen kiezen, of zelfs (B,A,()) , en we konden een ontledingsfunctie zoals de bovenstaande vinden die ook de regels volgde:

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

Dit komt omdat het product niet uniek is, maar uniek tot isomorfisme . Elke twee producten van A en B hoeven niet gelijk te zijn, maar ze moeten isomorf zijn. De twee verschillende producten die we zojuist hebben gedefinieerd (A,B) en (B,A,()) zijn bijvoorbeeld isomorf:

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

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

Uniciteit van de ontbinding

Het is belangrijk op te merken dat ook de ontledingsfunctie uniek moet zijn. Er zijn typen die alle regels volgen die vereist zijn om product te zijn, maar de ontleding is niet uniek. Als een voorbeeld kunnen we proberen (A,(B,Bool)) met projecties fst fst . snd als een product van A en B :

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

We kunnen controleren of het werkt:

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

Maar het probleem is dat we een andere ontbinding hadden kunnen schrijven, namelijk:

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

En omdat de ontleding niet uniek is , (A,(B,Bool)) is niet het product van A en B in Hask

Soorten coproducten in Hask

Intuïtie

Het categorische product van twee typen A en B moet de minimale informatie bevatten die nodig is om een instantie van type A of type B te bevatten . We kunnen nu zien dat het intuïtieve coproduct van twee typen Either ab moet zijn. Andere kandidaten, zoals Either a (b,Bool) , zouden een deel van onnodige informatie bevatten en ze zouden niet minimaal zijn.

De formele definitie is afgeleid van de categorische definitie van coproduct.

Categorische coproducten

Een categorisch coproduct is het dubbele begrip van een categorisch product. Het wordt rechtstreeks verkregen door alle pijlen in de definitie van het product om te keren. Het coproduct van twee objecten X , Y is een ander object Z met twee insluitsels: i_1: X → Z en i_2: Y → Z ; zodat elke andere twee morfismen van X en Y naar een ander object op unieke wijze ontleden door die insluitsels. Met andere woorden, als er twee morfismen f₁ zijn: X → W en f₂: Y → W , bestaat er een uniek morfisme g: Z → W zodat g ○ i₁ = f₁ en g ○ i₂ = f₂

Coproducts in Hask

De vertaling in de categorie Hask is vergelijkbaar met de vertaling van het product:

-- 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

Het coproducttype van twee typen A en B in Hask is Either ab of een ander type isomorf:

-- 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 

Haskell-toepassing in termen van categorietheorie

Met een Haskell's Functor kan elk type a (een object van Hask ) worden toegewezen aan een type F a en ook een functie a -> b (een morfisme van Hask ) worden toegewezen aan een functie met type F a -> F b . Dit komt overeen met een definitie van categorietheorie in die zin dat functor de basisstructuur van de categorie behoudt.

Een monoidale categorie is een categorie die wat extra structuur heeft:

• Een tensorproduct (zie Product van typen in Hask )
• Een tensor-eenheid (eenheidsobject)

Met een paar als ons product, kan deze definitie op de volgende manier worden vertaald naar Haskell:

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

De Applicative klasse is gelijk aan deze Monoidal klasse en kan dus worden geïmplementeerd in termen van:

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