Haskell Language
Kategoriteori

Kategoriteori som ett system för att organisera abstraktion

Kategoriteori är en modern matematisk teori och en gren av abstrakt algebra med inriktning på sambandets och relationens natur. Det är användbart för att ge solida grunder och vanliga språk för många återanvändbara programmeringsabstraktioner. Haskell använder kategoriteori som inspiration för några av de grundläggande typglasögon som finns tillgängliga både i standardbiblioteket och i flera populära tredjepartsbibliotek.

Ett exempel

Functor typklass säger att om en typ F Functor (för vilken vi skriver Functor F ) så har vi en generisk operation

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

vilket låter oss "kartlägga" över F Den normala (men ofullkomliga) intuitionen är att F a är en behållare full av värden av typ a och fmap låter oss tillämpa en transformation på vart och ett av dessa innehållande element. Ett exempel är 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

Med tanke på denna intuition är en vanlig fråga "varför inte kalla Functor något uppenbart som Mappable ?".

En antydan till kategoriteori

Anledningen är att Functor passar in i en uppsättning vanliga strukturer i kategoriteori och därför genom att kalla Functor "Functor" kan vi se hur den ansluter till denna djupare kropp av kunskap.

I synnerhet är kategoriteori mycket upptagen av idén om pilar från en plats till en annan. I Haskell är den viktigaste uppsättningen av pilar funktionspilarna a -> b . En vanlig sak att studera i kategoriteori är hur en uppsättning pilar förhåller sig till en annan uppsättning. Speciellt för alla typer av konstruktörer F är pilaruppsättningen med formen F a -> F b också intressanta.

Så en Functor är vilken som helst F så att det finns en koppling mellan normala Haskell-pilarna a -> b och de F specifika pilarna Fa F a -> F b . Anslutningen definieras av fmap och vi känner också igen några få lagar som måste hålla

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

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

Alla dessa lagar härrör naturligtvis från kategoritetsteoretisk tolkning av Functor och skulle inte vara så uppenbart nödvändiga om vi bara tänkte på Functor som avser "kartläggning av element".

Definition av en kategori

En kategori C består av:

• En samling av objekt som heter Obj(C) ;
• En samling (kallad Hom(C) ) av morfismer mellan dessa objekt. Om a och b är i Obj(C) , betecknas vanligtvis en morfism f i Hom(C) f : a -> b , och samlingen av all morfism mellan a och b betecknas hom(a,b) ;
• En speciell morfism som kallas identitetsmorfismen - för varje a : Obj(C) finns det en morfism- id : a -> a ;
• En kompositionsoperatör ( . ) Som tar två morfismer f : a -> b , g : b -> c och producerar en morfism a -> c

som följer följande lagar:

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

Med andra ord, komposition med identitetsmorfismen (till vänster eller höger) förändrar inte den andra morfismen, och kompositionen är associerande.

I Haskell definieras Category som ett typkategori i 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

I detta fall cat :: k -> k -> * objektiverar morfismförhållandet - det finns en morfism cat ab om och bara om cat ab är bebodd (dvs. har ett värde). a , b och c finns alla i Obj(C) . Obj(C) sig representeras av typen k - till exempel när k ~ * , som vanligtvis är fallet, är objekt typer.

Det kanoniska exemplet på en kategori i Haskell är funktionskategorin:

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

Ett annat vanligt exempel är Category för Kleisli pilar för en 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-typer som kategori

Definition av kategorin

Haskell-typerna tillsammans med funktioner mellan typerna bildar (nästan †) en kategori. Vi har en identitetsmorfism (funktion) ( id :: a -> a ) för varje objekt (typ) a ; och sammansättning av morfismer ( (.) :: (b -> c) -> (a -> b) -> a -> c ), som följer kategorilagar:

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

Vi kallar vanligtvis denna kategori Hask .

isomorfier

I kategoriteori har vi en isomorfism när vi har en morfism som har en omvänd, med andra ord finns det en morfism som kan komponeras med den för att skapa identiteten. I Hask utgör detta ett par morfismer f , g så att:

 f . g == id == g . f

Om vi hittar ett par sådana morfismer mellan två typer, kallar vi dem isomorfa för varandra .

Ett exempel på två isomorfa typer skulle vara ((),a) och a för vissa a . Vi kan konstruera de två morfismerna:

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

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

Och vi kan kontrollera att f . g == id == g . f .

funktorer

En funktor, i kategoriteori, går från en kategori till en annan och kartlägger objekt och morfismer. Vi arbetar bara med en kategori, kategorin Hask av Haskell-typer, så vi kommer att se bara funktorer från Hask till Hask , de funktorer, vars ursprung och destinationskategori är desamma, kallas endofunktorer . Våra endofunktorer kommer att vara de polymorfa typerna som tar en typ och returnerar en annan:

F :: * -> *

Att följa de kategoriska funktorlagarna (bevara identiteter och sammansättning) motsvarar att följa Haskell funktorlagar:

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

Så vi har till exempel att [] , Maybe eller (-> r) är funktorer i Hask .

monader

En monad i kategoriteori är en monoid i kategorin endofunktorer . Denna kategori har endofunktorer som objekt F :: * -> * och naturliga transformationer (transformationer mellan dem för alla forall a . F a -> G a ) som morfismer.

Ett monoidobjekt kan definieras i en monoidkategori och är en typ som har två morfismer:

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

Vi kan översätta detta ungefär till kategorin Hask-endofunktorer som:

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

Och att följa monadlagarna är likvärdigt med att följa de kategoriska monoidobjektlagarna.

† Faktum är att klassen för alla typer tillsammans med klassen av funktioner mellan typer inte strikt bildar en kategori i Haskell, på grund av existerande av undefined . Vanligtvis åtgärdas detta genom att helt enkelt definiera objekten i Hask- kategorin som typer utan bottenvärden, vilket utesluter icke-avslutande funktioner och oändliga värden (kodata). För en detaljerad diskussion om detta ämne, se här .

Produkt av typer i Hask

Kategoriska produkter

I kategoriteori är produkten av två objekt X , Y ett annat objekt Z med två projektioner: π₁: Z → X och π2: Z → Y ; så att alla andra två morfismer från ett annat objekt sönderdelas unikt genom dessa prognoser. Med andra ord, om det finns f₁: W → X och f2: W → Y , finns en unik morfism g: W → Z så att π₁ ○ g = f₁ och π2 ○ g = f2 .

Produkter i Hask

Detta översätter till Hask- kategorin av Haskell-typer enligt följande, Z är produkt av A , B när:

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

Produkttypen av två typer A , B , som följer lagen ovan, är tupeln för de två typerna (A,B) , och de två projektionerna är fst och snd . Vi kan kontrollera att den följer ovanstående regel, om vi har två funktioner f1 :: W -> A och f2 :: W -> B vi sönderdela dem unikt på följande sätt:

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

Och vi kan kontrollera att nedbrytningen är korrekt:

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

Unikhet fram till isomorfism

Valet av (A,B) som produkten av A och B är inte unikt. Ett annat logiskt och likvärdigt val skulle ha varit:

data Pair a b = Pair a b

Dessutom kunde vi också ha valt (B,A) som produkten, eller till och med (B,A,()) , och vi kunde hitta en sönderdelningsfunktion som ovan enligt följande regler:

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

Detta beror på att produkten inte är unik utan unik fram till isomorfism . Varje två produkter av A och B behöver inte vara lika, men de bör vara isomorfa. Som ett exempel är de två olika produkterna vi just har definierat, (A,B) och (B,A,()) , isomorfa:

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

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

Det unika med nedbrytningen

Det är viktigt att notera att även nedbrytningsfunktionen måste vara unik. Det finns typer som följer alla regler som krävs för att vara produkt, men nedbrytningen är inte unik. Som exempel kan vi försöka använda (A,(B,Bool)) med projektioner fst fst . snd som en produkt av A och B :

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

Vi kan kontrollera att det fungerar:

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

Men problemet här är att vi kunde ha skrivit en annan nedbrytning, nämligen:

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

Och eftersom nedbrytningen inte är unik (A,(B,Bool)) är inte produkten av A och B i Hask

Koproduktion av typer i Hask

Intuition

Den kategoriska produkten av två typer A och B bör innehålla den minimala information som är nödvändig för att innehålla en instans av typ A eller B. Vi ser nu att den intuitiva samprodukten av två typer borde vara Either ab . Andra kandidater, som Either a (b,Bool) , skulle innehålla en del av onödig information, och de skulle inte vara minimala.

Den formella definitionen härstammar från den kategoriska definitionen av koprodukt.

Kategoriska koprodukter

En kategorisk samprodukt är den dubbla uppfattningen om en kategorisk produkt. Det erhålls direkt genom att vända alla pilar i definitionen av produkten. Koprodukten av två objekt X , Y är ett annat objekt Z med två inneslutningar: i_1: X → Z och i_2: Y → Z ; så att alla andra två morfismer från X och Y till ett annat objekt sönderdelas unikt genom dessa inneslutningar. Med andra ord, om det finns två morfismer f: X → W och f2: Y → W , existerar en unik morfism g: Z → W så att g ○ i₁ = f₁ och g ○ i2 = f2

Koprodukter i Hask

Översättningen till Hask- kategorin liknar översättningen av produkten:

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

Koproduktstypen av två typer A och B i Hask är Either ab eller någon annan typ som är isomorf för det:

-- 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 tillämplig när det gäller kategoriteori

En Haskells Functor tillåter en att kartlägga vilken typ som helst av a (ett objekt av Hask ) till en typ F a och också kartlägga en funktion a -> b (en morfism av Hask ) till en funktion med typ F a -> F b . Detta motsvarar en kategorityrdefinition i en mening att funktorn bevarar grundläggande kategoristruktur.

En monoidal kategori är en kategori som har en viss ytterligare struktur:

• En tensorprodukt (se Produkt av typer i Hask )
• En tensorenhet (enhetsobjekt)

Med ett par som vår produkt kan denna definition översättas till Haskell på följande sätt:

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

Den Applicative klassen motsvarar denna Monoidal och kan därför implementeras i termer av den:

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