Haskell Language
Algèbre de type

Nombres naturels en algèbre de type

Nous pouvons établir un lien entre les types Haskell et les nombres naturels. Cette connexion peut être faite en attribuant à chaque type le nombre d'habitants qu'il possède.

Types d'union finis

Pour les types finis, il suffit de voir que l'on peut attribuer un type naturel à chaque nombre, en fonction du nombre de constructeurs. Par exemple:

type Color = Red | Yellow | Green

serait 3 . Et le type Bool serait 2 .

type Bool = True | False

Unicité jusqu'à l'isomorphisme

Nous avons vu que plusieurs types correspondraient à un seul numéro, mais dans ce cas, ils seraient isomorphes. C'est-à-dire qu'il y aurait une paire de morphismes f et g , dont la composition serait l'identité, reliant les deux types.

f :: a -> b
g :: b -> a

f . g == id == g . f

Dans ce cas, nous dirions que les types sont isomorphes . Nous considérerons deux types égaux dans notre algèbre tant qu'ils sont isomorphes.

Par exemple, deux représentations différentes du nombre deux sont trivialement isomorphes:

type Bit  = I    | O
type Bool = True | False

bitValue :: Bit -> Bool
bitValue I = True
bitValue O = False

booleanBit :: Bool -> Bit
booleanBit True  = I
booleanBit False = O

Parce que nous pouvons voir bitValue . booleanBit == id == booleanBit . bitValue

Un et zéro

La représentation du nombre 1 est évidemment un type avec un seul constructeur. Dans Haskell, ce type est canoniquement le type () , appelé Unit. Tout autre type avec un seul constructeur est isomorphe à () .

Et notre représentation de 0 sera un type sans constructeurs. C'est le type Void dans Haskell, tel que défini dans Data.Void . Cela équivaudrait à un type non habité, sans constructeurs de données:

data Void

Ajout et multiplication

L'addition et la multiplication ont des équivalents dans ce type algèbre. Ils correspondent aux unions marquées et aux types de produits .

data Sum a b = A a | B b
data Prod a b = Prod a b

Nous pouvons voir comment le nombre d'habitants de chaque type correspond aux opérations de l'algèbre.

De manière équivalente, nous pouvons utiliser Either et (,) comme constructeurs de type pour l'addition et la multiplication. Ils sont isomorphes à nos types précédemment définis:

type Sum' a b = Either a b
type Prod' a b = (a,b)

Les résultats attendus de l'addition et de la multiplication sont suivis par le type algèbre jusqu'à l'isomorphisme. Par exemple, on peut voir un isomorphisme entre 1 + 2, 2 + 1 et 3; comme 1 + 2 = 3 = 2 + 1.

data Color = Red | Green | Blue

f :: Sum () Bool -> Color
f (Left ())     = Red
f (Right True)  = Green
f (Right False) = Blue

g :: Color -> Sum () Bool
g Red   = Left ()
g Green = Right True
g Blue  = Right False

f' :: Sum Bool () -> Color
f' (Right ())   = Red
f' (Left True)  = Green
f' (Left False) = Blue

g' :: Color -> Sum Bool ()
g' Red   = Right ()
g' Green = Left True
g' Blue  = Left False

Règles d'addition et de multiplication

Les règles communes de commutativité, associativité et distributivité sont valables car il existe des isomorphismes triviaux entre les types suivants:

-- Commutativity
Sum a b           <=> Sum b a
Prod a b          <=> Prod b a
-- Associativity
Sum (Sum a b) c   <=> Sum a (Sum b c)
Prod (Prod a b) c <=> Prod a (Prod b c)
-- Distributivity
Prod a (Sum b c)  <=> Sum (Prod a b) (Prod a c)

Types récursifs

Des listes

Les listes peuvent être définies comme suit:

data List a = Nil | Cons a (List a) 

Si nous traduisons cela dans notre algèbre de type, nous obtenons

Liste (a) = 1 + a * Liste (a)

Mais nous pouvons maintenant substituer plusieurs fois List (a) dans cette expression pour obtenir:

Liste (a) = 1 + a + a * a + a * a * a + a * a * a * a + ...

Cela a du sens si nous voyons une liste comme un type qui ne peut contenir qu’une valeur, comme dans [] ; ou toute valeur de type a , comme dans [x] ; ou deux valeurs de type a , comme dans [x,y] ; etc. La définition théorique de List que nous devrions en tirer serait:

-- Not working Haskell code!
data List a = Nil
            | One a
            | Two a a
            | Three a a a 
            ...

Des arbres

Nous pouvons faire la même chose avec les arbres binaires, par exemple. Si nous les définissons comme:

data Tree a = Empty | Node a (Tree a) (Tree a)

Nous obtenons l'expression:

Arbre (a) = 1 + a * Arbre (a) * Arbre (a)

Et si nous faisons les mêmes substitutions encore et encore, nous obtiendrons la séquence suivante:

Arbre (a) = 1 + a + 2 (a * a) + 5 (a * a * a) + 14 (a * a * a * a) + ...

Les coefficients que nous obtenons ici correspondent à la séquence des nombres catalans, et le nième nombre catalan est précisément le nombre d'arbres binaires possibles avec n nœuds.

Dérivés

La dérivée d'un type est le type de son type de contexte à un trou. C'est le type que nous obtiendrions si nous faisons disparaître une variable de type à chaque point et additionnons les résultats.

Par exemple, nous pouvons prendre le triple type (a,a,a) et le dériver, en obtenant

data OneHoleContextsOfTriple = (a,a,()) | (a,(),a) | ((),a,a)

Ceci est cohérent avec notre définition habituelle de la dérivation, comme suit:

d / da (a * a * a) = 3 * a * a

Plus d'informations sur ce sujet peuvent être lues sur cet article .

Les fonctions

Les fonctions peuvent être considérées comme exponentielles dans notre algèbre. Comme nous pouvons le voir, si nous prenons un type a avec n instances et un type b avec m instances, le type a -> b aura m a -> b la puissance de n instances.

Par exemple, Bool -> Bool est isomorphe à (Bool,Bool) , comme 2 * 2 = 2².

iso1 :: (Bool -> Bool) -> (Bool,Bool)
iso1 f = (f True,f False)

iso2 :: (Bool,Bool) -> (Bool -> Bool)
iso2 (x,y) = (\p -> if p then x else y)