Haskell Language
Théorie des catégories
Recherche…
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. Sia
etb
sont dansObj(C)
, alors un morphismef
dansHom(C)
est typiquement notéf : a -> b
, et la collection de tout morphisme entrea
etb
est notéehom(a,b)
; - Un morphisme spécial appelé morphisme de l' identité - pour tout
a : Obj(C)
il existe unid : a -> a
morphismeid : a -> a
; - Un opérateur de composition (
.
), Prenant deux morphismesf : a -> b
,g : b -> c
et produisant un morphismea -> 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)