Haskell Language
Type algebra

Natuurlijke getallen in type algebra

We kunnen een verband leggen tussen de Haskell-types en de natuurlijke getallen. Via deze verbinding kan aan elk type het aantal inwoners worden toegewezen.

Eindige unietypes

Voor eindige typen is het voldoende om te zien dat we aan elk getal een natuurlijk type kunnen toewijzen, gebaseerd op het aantal constructeurs. Bijvoorbeeld:

type Color = Red | Yellow | Green

zou 3 zijn . En het Bool type zou 2 zijn .

type Bool = True | False

Uniek tot isomorfisme

We hebben gezien dat meerdere typen zouden overeenkomen met een enkel nummer, maar in dit geval zouden ze isomorf zijn. Dit wil zeggen dat er een paar morfismen f en g zouden zijn, waarvan de samenstelling de identiteit zou zijn, die de twee typen met elkaar verbindt.

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

f . g == id == g . f

In dit geval zouden we zeggen dat de typen isomorf zijn . We zullen twee soorten in onze algebra als gelijk beschouwen zolang ze isomorf zijn.

Twee verschillende representaties van het nummer twee zijn bijvoorbeeld triviaal isomorf:

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

Omdat we bitValue . booleanBit == id == booleanBit . bitValue kunnen zien bitValue . booleanBit == id == booleanBit . bitValue

Eén en nul

De weergave van het nummer 1 is duidelijk een type met slechts één constructor. In Haskell is dit type canoniek het type () , genaamd Unit. Elk ander type met slechts één constructor is isomorf voor () .

En onze weergave van 0 zal een type zijn zonder constructors. Dit is het type Leegte in Haskell, zoals gedefinieerd in Data.Void . Dit zou equivalent zijn aan een onbewoond type, zonder gegevensconstructeurs:

data Void

Optellen en vermenigvuldigen

De optelling en vermenigvuldiging hebben equivalenten in dit type algebra. Ze komen overeen met de getagde vakbonden en producttypen .

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

We kunnen zien hoe het aantal inwoners van elk type overeenkomt met de activiteiten van de algebra.

Evenzo kunnen we Either en (,) als type constructors voor de optelling en de vermenigvuldiging. Ze zijn isomorf voor onze eerder gedefinieerde typen:

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

De verwachte resultaten van optelling en vermenigvuldiging worden gevolgd door het type algebra tot isomorfisme. We kunnen bijvoorbeeld een isomorfisme zien tussen 1 + 2, 2 + 1 en 3; als 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

Regels voor optellen en vermenigvuldigen

De gemeenschappelijke regels van commutativiteit, associativiteit en distributiviteit zijn geldig omdat er triviale isomorfismen zijn tussen de volgende typen:

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

Recursieve typen

lijsten

Lijsten kunnen worden gedefinieerd als:

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

Als we dit vertalen naar ons type algebra, krijgen we

Lijst (a) = 1 + a * Lijst (a)

Maar we kunnen nu in deze uitdrukking meerdere keren Lijst (a) vervangen om het volgende te krijgen:

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

Dit is logisch als we een lijst zien als een type dat slechts één waarde kan bevatten, zoals in [] ; of elke waarde van type a , zoals in [x] ; of twee waarden van type a , zoals in [x,y] ; enzovoorts. De theoretische definitie van Lijst die we daar moeten krijgen, zou zijn:

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

bomen

We kunnen bijvoorbeeld hetzelfde doen met binaire bomen. Als we ze definiëren als:

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

We krijgen de uitdrukking:

Boom (a) = 1 + a * Boom (a) * Boom (a)

En als we steeds opnieuw dezelfde substituties uitvoeren, zouden we de volgende volgorde krijgen:

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

De coëfficiënten die we hier krijgen, komen overeen met de Catalaanse getallenreeks en het n-de Catalaanse getal is precies het aantal mogelijke binaire bomen met n knooppunten.

derivaten

De afgeleide van een type is het type van zijn type een-gat contexten. Dit is het type dat we zouden krijgen als we een typevariabele op elk mogelijk punt laten verdwijnen en de resultaten optellen.

Als voorbeeld kunnen we het drievoudige type (a,a,a) en het afleiden, verkrijgen

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

Dit is coherent met onze gebruikelijke definitie van afleiding, zoals:

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

Meer over dit onderwerp is te lezen in dit artikel .

functies

Functies kunnen worden gezien als exponentiële functies in onze algebra. Zoals we kunnen zien, als we een type a met n instanties en een type b met m instanties, zal het type a -> b m hebben tot de macht van n instanties.

Als voorbeeld is Bool -> Bool isomorf aan (Bool,Bool) , als 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)