Haskell Language
Teoria delle categorie

Teoria delle categorie come sistema per organizzare l'astrazione

La teoria delle categorie è una moderna teoria matematica e una branca dell'algebra astratta focalizzata sulla natura della connessione e della relazione. È utile per dare basi solide e linguaggio comune a molte astrazioni di programmazione altamente riutilizzabili. Haskell utilizza la teoria delle categorie come fonte di ispirazione per alcune delle classifiche di base disponibili sia nella libreria standard sia in numerose librerie di terze parti.

Un esempio

La Functor Functor dice che se un tipo F crea un'istanza di Functor (per la quale scriviamo Functor F ), allora abbiamo un'operazione generica

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

che ci permette di "mappare" su F L'intuizione standard (ma imperfetta) è che F a è un contenitore pieno di valori di tipo a e fmap permette di applicare una trasformazione a ciascuno di questi elementi contenuti. Un esempio è 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

Data questa intuizione, una domanda comune è "perché non chiamare Functor qualcosa di ovvio come Mappable ?".

Un pizzico di teoria delle categorie

La ragione è che Functor si inserisce in una serie di strutture comuni nella teoria delle categorie e quindi chiamando Functor "Functor" possiamo vedere come si collega a questo corpo di conoscenza più profondo.

In particolare, la teoria delle categorie è fortemente interessata all'idea di frecce da un luogo all'altro. In Haskell, la più importante serie di frecce sono le frecce di funzione a -> b . Una cosa comune da studiare nella teoria delle categorie è come un set di frecce si riferisce a un altro set. In particolare, per qualsiasi tipo di costruttore F , anche l'insieme di frecce della forma F a -> F b è interessante.

Quindi un Functor è qualsiasi F tale che ci sia una connessione tra le normali frecce Haskell a -> b e le frecce specifiche F F a -> F b . La connessione è definita da fmap e riconosciamo anche alcune leggi che devono contenere

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

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

Tutte queste leggi derivano naturalmente dall'interpretazione Teorica di Categoria di Functor e non sarebbero ovviamente necessarie se pensassimo a Functor in relazione alla "mappatura degli elementi".

Definizione di una categoria

Una categoria C comprende:

• Una raccolta di oggetti chiamata Obj(C) ;
• Una collezione (chiamata Hom(C) ) di morfismi tra questi oggetti. Se a e b sono in Obj(C) , allora un morfismo f in Hom(C) è tipicamente denotato f : a -> b , e l'insieme di tutti i morfismi tra a e b è denotato hom(a,b) ;
• Uno speciale morfismo chiamato morfismo identitario - per ogni a : Obj(C) esiste un id : a -> a morfismo id : a -> a ;
• Un operatore di composizione ( . ), Prendendo due morfismi f : a -> b , g : b -> c e producendo un morfismo a -> c

che obbediscono alle seguenti leggi:

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

In altre parole, la composizione con il morfismo identitario (a sinistra oa destra) non cambia l'altro morfismo e la composizione è associativa.

In Haskell, la Category è definita come un 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 questo caso, cat :: k -> k -> * oggettifica la relazione morfismo - esiste un morfismo cat ab se e solo se cat ab è abitato (cioè ha un valore). a , b e c sono tutti in Obj(C) . Obj(C) stesso è rappresentato dal tipo k - per esempio, quando k ~ * , come è tipicamente il caso, gli oggetti sono tipi.

L'esempio canonico di una categoria in Haskell è la categoria di funzioni:

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

Un altro esempio comune è la Category di frecce di Kleisli per una 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 digita come categoria

Definizione della categoria

I tipi di Haskell e le funzioni tra i tipi formano (quasi †) una categoria. Abbiamo un morfismo identitario (funzione) ( id :: a -> a ) per ogni oggetto (tipo) a ; e composizione dei morfismi ( (.) :: (b -> c) -> (a -> b) -> a -> c ), che obbediscono alle leggi di categoria:

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

Solitamente chiamiamo questa categoria Hask .

isomorfismi

Nella teoria delle categorie, abbiamo un isomorfismo quando abbiamo un morfismo che ha un inverso, in altre parole, c'è un morfismo che può essere composto con esso per creare l'identità. In Hask questo equivale ad avere un paio di morfismi f , g tali che:

 f . g == id == g . f

Se troviamo una coppia di tali morfismi tra due tipi, li chiamiamo isomorfi l'uno con l'altro .

Un esempio di due tipi isomorfi sarebbe ((),a) e a per alcuni a . Possiamo costruire i due morfismi:

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

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

E possiamo controllare che f . g == id == g . f .

funtori

Un funtore, nella teoria delle categorie, passa da una categoria all'altra, mappando oggetti e morfismi. Stiamo lavorando solo su una categoria, la categoria Hask di tipi Haskell, quindi vedremo solo i funtori da Hask a Hask , quei funtori, la cui origine e destinazione sono gli stessi, sono chiamati endofuntor . I nostri endofuncatori saranno i tipi polimorfici che prendono un tipo e ne restituiscono un altro:

F :: * -> *

Obbedire alle leggi del funtore categoriale (preservare identità e composizione) equivale a obbedire alle leggi del funtore di Haskell:

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

Quindi, abbiamo, per esempio, che [] , Maybe o (-> r) sono funtori in Hask .

monadi

Una monade nella teoria delle categorie è un monoide nella categoria dei endofuntor . Questa categoria ha endofuncori come oggetti F :: * -> * e trasformazioni naturali (trasformazioni tra loro per tutti forall a . F a -> G a ) come morfismi.

Un oggetto monoide può essere definito su una categoria monoidale ed è un tipo con due morfismi:

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

Possiamo tradurre questo approssimativamente alla categoria dei endofunzionisti Hask come:

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

E, obbedire alle leggi della monade equivale ad obbedire alle leggi categoriali degli oggetti monoidi.

† In effetti, la classe di tutti i tipi insieme alla classe di funzioni tra i tipi non formano strettamente una categoria in Haskell, a causa dell'esistenza di undefined . Solitamente questo viene risolto semplicemente definendo gli oggetti della categoria Hask come tipi senza valori di fondo, che esclude funzioni non terminanti e valori infiniti (codi). Per una discussione dettagliata di questo argomento, vedere qui .

Prodotto di tipi in Hask

Prodotti categoriali

Nella teoria delle categorie, il prodotto di due oggetti X , Y è un altro oggetto Z con due proiezioni: π₁: Z → X e π₂: Z → Y ; in modo tale che qualsiasi altro morfismo di un altro oggetto si decomponga in modo univoco attraverso tali proiezioni. In altre parole, se esiste f₁: W → X e f₂: W → Y , esiste un morfismo unico g: W → Z tale che π₁ ○ g = f₁ e π₂ ○ g = f₂ .

Prodotti in Hask

Questo si traduce nella categoria Hask dei tipi Haskell come segue, Z è un prodotto di A , B quando:

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

Il tipo di prodotto di due tipi A , B , che segue la legge sopra riportata, è la tupla dei due tipi (A,B) e le due proiezioni sono fst e snd . Possiamo verificare che segua la regola precedente, se abbiamo due funzioni f1 :: W -> A e f2 :: W -> B possiamo decomporle in modo univoco come segue:

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

E possiamo controllare che la decomposizione sia corretta:

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

Unicità fino all'isomorfismo

La scelta di (A,B) come prodotto di A e B non è unica. Un'altra scelta logica ed equivalente sarebbe stata:

data Pair a b = Pair a b

Inoltre, avremmo potuto anche scegliere (B,A) come prodotto, o anche (B,A,()) , e potremmo trovare una funzione di scomposizione come sopra anche seguendo le regole:

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

Questo perché il prodotto non è unico ma unico fino all'isomorfismo . Ogni due prodotti di A e B non devono essere uguali, ma dovrebbero essere isomorfi. Ad esempio, i due diversi prodotti che abbiamo appena definito, (A,B) e (B,A,()) , sono isomorfi:

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

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

Unicità della decomposizione

È importante osservare che anche la funzione di scomposizione deve essere unica. Ci sono tipi che seguono tutte le regole richieste per essere prodotto, ma la decomposizione non è unica. Ad esempio, possiamo provare a usare (A,(B,Bool)) con le proiezioni fst fst . snd come prodotto di A e B :

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

Possiamo verificare che funzioni:

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

Ma il problema qui è che avremmo potuto scrivere un'altra decomposizione, vale a dire:

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

E, poiché la decomposizione non è unica , (A,(B,Bool)) non è il prodotto di A e B in Hask

Coproduzione di tipi in Hask

Intuizione

Il prodotto categoriale di due tipi A e B dovrebbe contenere le informazioni minime necessarie per contenere all'interno di un'istanza di tipo A o di tipo B. Ora possiamo vedere che il coprodotto intuitivo di due tipi dovrebbe essere Either ab . Altri candidati, come ad esempio Either a (b,Bool) , conterrebbero una parte di informazioni non necessarie e non sarebbero minimali.

La definizione formale deriva dalla definizione categoriale di coproduzione.

Coprodotti categoriali

Un coprodotto categoriale è la duplice nozione di prodotto categoriale. Si ottiene direttamente invertendo tutte le frecce nella definizione del prodotto. Il coprodotto di due oggetti X , Y è un altro oggetto Z con due inclusioni: i_1: X → Z e i_2: Y → Z ; in modo tale che qualsiasi altro due morfismi da X e Y a un altro oggetto si decompongano in modo univoco attraverso quelle inclusioni. In altre parole, se ci sono due morfismi f₁: X → W e f₂: Y → W , esiste un morfismo unico g: Z → W tale che g ○ i₁ = f₁ e g ○ i₂ = f₂

Coproduttori in Hask

La traduzione nella categoria Hask è simile alla traduzione del prodotto:

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

Il tipo di coproduzione di due tipi A e B in Hask è Either ab o un qualsiasi altro tipo isomorfo ad esso:

-- 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 Applicativo in termini di teoria delle categorie

A Haskell's Functor consente di mappare qualsiasi tipo a (un oggetto di Hask ) a un tipo F a e anche mappare una funzione a -> b (un morfismo di Hask ) a una funzione con tipo F a -> F b . Ciò corrisponde a una definizione di teoria di categoria, nel senso che functor conserva la struttura di categoria di base.

Una categoria monoidale è una categoria che ha una struttura aggiuntiva :

• Un prodotto tensoriale (vedi Prodotto di tipi in Hask )
• Un'unità tensoriale (oggetto unitario)

Assumendo una coppia come nostro prodotto, questa definizione può essere tradotta in Haskell nel modo seguente:

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

La classe Applicative è equivalente a questa Monoidal e quindi può essere implementata in termini di essa:

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