Haskell Language
Théorie des catégories

La théorie des catégories comme système d'organisation de l'abstraction

La théorie des catégories est une théorie mathématique moderne et une branche de l'algèbre abstraite axée sur la nature de la connectivité et de la relation. Il est utile pour donner des bases solides et un langage commun à de nombreuses abstractions de programmation hautement réutilisables. Haskell utilise la théorie des catégories comme source d'inspiration pour certaines des classes de base disponibles à la fois dans la bibliothèque standard et dans plusieurs bibliothèques tierces populaires.

Un exemple

La Functor Functor dit que si un type F instancie Functor (pour lequel on écrit Functor F ), alors nous avons une opération générique

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

ce qui nous permet de "carte" sur F L'intuition standard (mais imparfaite) est que F a est un conteneur plein de valeurs de type a et fmap nous permet d'appliquer une transformation à chacun de ces éléments contenus. Un exemple est Maybe - 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

Compte tenu de cette intuition, une question commune est "pourquoi ne pas appeler Functor quelque chose d'évident comme Mappable ?".

Un soupçon de théorie des catégories

La raison en est que Functor s'intègre dans un ensemble de structures communes à la théorie des catégories et donc, en appelant Functor "Functor", nous pouvons voir comment il se connecte à ce corpus de connaissances plus profond.

En particulier, la théorie des catégories est très concernée par l’idée des flèches d’un endroit à un autre. Dans Haskell, les flèches les plus importantes sont les flèches de fonction a -> b . Une chose courante à étudier dans la théorie des catégories est la relation entre un ensemble de flèches et un autre ensemble. En particulier, pour tout constructeur de type F , l'ensemble des flèches de la forme F a -> F b est également intéressant.

Ainsi , un Functor est une F telle qu'il ya une connexion entre Haskell normale flèches a -> b et F flèches Spécifiques F a -> F b . La connexion est définie par fmap et nous reconnaissons également quelques lois qui doivent tenir

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

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

Toutes ces lois découlent naturellement de l'interprétation théorique de Functor et ne seraient évidemment pas nécessaires si l'on pensait seulement à Functor comme se rapportant à la "cartographie des éléments".

Définition d'une catégorie

Une catégorie C comprend:

• Une collection d'objets appelée Obj(C) ;
• Une collection (appelée Hom(C) ) de morphismes entre ces objets. Si a et b sont dans Obj(C) , alors un morphisme f dans Hom(C) est typiquement noté f : a -> b , et la collection de tout morphisme entre a et b est notée hom(a,b) ;
• Un morphisme spécial appelé morphisme de l' identité - pour tout a : Obj(C) il existe un id : a -> a morphisme id : a -> a ;
• Un opérateur de composition ( . ), Prenant deux morphismes f : a -> b , g : b -> c et produisant un morphisme a -> c

qui obéissent aux lois suivantes:

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

En d'autres termes, la composition avec le morphisme identitaire (à gauche ou à droite) ne change pas l'autre morphisme, et la composition est associative.

Dans Haskell, la Category est définie comme une classe de type dans 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

Dans ce cas, cat :: k -> k -> * objective la relation de morphisme - il existe un morphisme cat ab si et seulement si cat ab est habité (c'est-à-dire a une valeur). a , b et c sont tous dans Obj(C) . Obj(C) lui-même est représenté par le genre k - par exemple, lorsque k ~ * , comme c'est généralement le cas, les objets sont des types.

L'exemple canonique d'une catégorie dans Haskell est la catégorie de fonction:

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

Un autre exemple courant est la Category des flèches de Kleisli pour une 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)

Les types Haskell en tant que catégorie

Définition de la catégorie

Les types Haskell ainsi que les fonctions entre les types forment (presque †) une catégorie. Nous avons un morphisme d'identité (fonction) ( id :: a -> a ) pour chaque objet (type) a ; et composition des morphismes ( (.) :: (b -> c) -> (a -> b) -> a -> c ), qui obéissent aux lois de la catégorie:

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

Nous appelons généralement cette catégorie Hask .

Isomorphismes

En théorie des catégories, nous avons un isomorphisme lorsque nous avons un morphisme qui a un inverse, en d'autres termes, il existe un morphisme qui peut être composé avec lui pour créer l'identité. Dans Hask, cela revient à avoir une paire de morphismes f , g tels que:

 f . g == id == g . f

Si nous trouvons une paire de tels morphismes entre deux types, nous les appelons isomorphes les uns aux autres .

Un exemple de deux types isomorphes serait ((),a) et a pour certains a . Nous pouvons construire les deux morphismes:

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

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

Et on peut vérifier ça f . g == id == g . f .

Les foncteurs

Un foncteur, en théorie des catégories, passe d’une catégorie à une autre, mappant des objets et des morphismes. Nous travaillons uniquement sur une catégorie, la catégorie Hask de types Haskell, nous allons donc voir uniquement les foncteurs de Hask à Hask , ces foncteurs, dont l'origine et la catégorie de destination sont les mêmes, sont appelés endofuncteurs . Nos endofuncteurs seront les types polymorphes prenant un type et en renvoyant un autre:

F :: * -> *

Obéir aux lois des foncteurs catégoriels (préserver les identités et la composition) équivaut à obéir aux lois du foncteur Haskell:

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

Nous avons, par exemple, que [] , Maybe ou (-> r) sont des foncteurs dans Hask .

Monades

Une monade dans la théorie des catégories est un monoïde sur la catégorie des endofuncteurs . Cette catégorie a des endofuncteurs en tant qu'objets F :: * -> * et des transformations naturelles (les transformations entre eux pour tout forall a . F a -> G a ) en tant que morphismes.

Un objet monoïde peut être défini sur une catégorie monoïdale et est un type ayant deux morphismes:

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

Nous pouvons traduire cela grossièrement dans la catégorie des endofuncteurs Hask comme:

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

Et obéir aux lois de la monade équivaut à obéir aux lois catégoriques des objets monoïdes.

† En fait, la classe de tous les types ainsi que la classe des fonctions entre les types ne forment pas strictement une catégorie dans Haskell, en raison de l'existence de undefined . En règle générale, cela est résolu en définissant simplement les objets de la catégorie Hask en tant que types sans valeurs inférieures, ce qui exclut les fonctions non terminantes et les valeurs infinies (codata). Pour une discussion détaillée de ce sujet, voir ici .

Produit de types en Hask

Produits catégoriels

En théorie des catégories, le produit de deux objets X , Y est un autre objet Z avec deux projections: π₁: Z → X et π₂: Z → Y ; de sorte que tous les deux autres morphismes d'un autre objet se décomposent uniquement à travers ces projections. En d'autres termes, s'il existe f: W → X et f₂: W → Y , il existe un morphisme unique g: W → Z tel que π₁ ○ g = f₁ et π₂ ○ g = f₂ .

Produits en Hask

Cela se traduit dans la catégorie Hask des types Haskell comme suit, Z est le produit de A , B lorsque:

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

Le type de produit de deux types A , B , qui suit la loi indiquée ci-dessus, est le tuple des deux types (A,B) , et les deux projections sont fst et snd . On peut vérifier qu'il suit la règle ci-dessus, si on a deux fonctions f1 :: W -> A et f2 :: W -> B on peut les décomposer de la manière suivante:

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

Et on peut vérifier que la décomposition est correcte:

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

Unicité jusqu'à l'isomorphisme

Le choix de (A,B) comme produit de A et B n'est pas unique. Un autre choix logique et équivalent aurait été:

data Pair a b = Pair a b

De plus, nous aurions pu aussi choisir (B,A) comme produit, ou même (B,A,()) , et nous pourrions trouver une fonction de décomposition comme ci-dessus en suivant les règles:

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

C'est parce que le produit n'est pas unique mais unique jusqu'à l'isomorphisme . Tous les deux produits de A et B ne doivent pas nécessairement être égaux, mais ils doivent être isomorphes. Par exemple, les deux produits que nous venons de définir (A,B) et (B,A,()) sont isomorphes:

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

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

Unicité de la décomposition

Il est important de noter que la fonction de décomposition doit également être unique. Il existe des types qui suivent toutes les règles requises pour être produit, mais la décomposition n'est pas unique. Par exemple, nous pouvons essayer d'utiliser (A,(B,Bool)) avec des projections du fst fst . snd tant que produit de A et B :

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

Nous pouvons vérifier que cela fonctionne:

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

Mais le problème ici est que nous aurions pu écrire une autre décomposition, à savoir:

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

Et, comme la décomposition n'est pas unique , (A,(B,Bool)) n'est pas le produit de A et B dans Hask

Coproduit de types en Hask

Intuition

Le produit catégoriel de deux types A et B doit contenir les informations minimales nécessaires pour contenir une instance de type A ou B. Nous pouvons voir maintenant que le coproduit intuitif de deux types devrait être l'un Either ab l' Either ab . D'autres candidats, tels que Either a (b,Bool) , contiendraient une partie des informations inutiles et ne seraient pas minimes.

La définition formelle est dérivée de la définition catégorique du coproduit.

Coproduits catégoriels

Un coproduit catégorique est la double notion de produit catégorique. Il est obtenu directement en inversant toutes les flèches dans la définition du produit. Le coproduit de deux objets X , Y est un autre objet Z avec deux inclusions: i_1: X → Z et i_2: Y → Z ; de telle sorte que tous les deux morphismes de X et Y à un autre objet se décomposent uniquement à travers ces inclusions. En d'autres termes, s'il y a deux morphismes f₁: X → W et f₂: Y → W , il existe un morphisme unique g: Z → W tel que g ○ i₁ = f₁ et g ○ i₂ = f₂

Coproduits en Hask

La traduction dans la catégorie Hask est similaire à la traduction du produit:

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

Le type de coproduit de deux types A et B dans Hask est Either ab ou tout autre type isomorphe à celui-ci:

-- 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 Applicative en termes de théorie des catégories

Un Functor de Haskell permet de mapper n'importe quel type a (un objet de Hask ) à un type F a et de mapper une fonction a -> b (un morphisme de Hask ) sur une fonction de type F a -> F b . Cela correspond à une définition de théorie de catégorie dans un sens que functor préserve la structure de catégorie de base.

Une catégorie monoïdale est une catégorie qui a une structure supplémentaire :

• Un produit tenseur (voir Produit de types dans Hask )
• Une unité de tenseur (objet unitaire)

En prenant une paire comme notre produit, cette définition peut être traduite en Haskell de la manière suivante:

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

La classe Applicative est équivalente à celle du Monoidal et peut donc être implémentée en termes de:

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