Haskell Language
Skriv algebra

Naturliga siffror i typ algebra

Vi kan skapa en koppling mellan Haskell-typerna och de naturliga siffrorna. Denna anslutning kan göras genom att tilldela varje typ antalet invånare det har.

Finita facktyper

För ändliga typer räcker det med att se att vi kan tilldela en naturlig typ till varje nummer, baserat på antalet konstruktörer. Till exempel:

type Color = Red | Yellow | Green

skulle vara 3 . Och Bool typen skulle vara 2 .

type Bool = True | False

Unikhet fram till isomorfism

Vi har sett att flera typer skulle motsvara ett enda nummer, men i det här fallet skulle de vara isomorfa. Detta för att säga att det skulle finnas ett par morfismer f och g , vars sammansättning skulle vara identiteten, koppla de två typerna.

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

f . g == id == g . f

I det här fallet skulle vi säga att typerna är isomorfa . Vi kommer att betrakta två typer som är lika i vår algebra så länge de är isomorfa.

Till exempel är två olika representationer av nummer två triviellt isomorfa:

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

Eftersom vi kan se bitValue . booleanBit == id == booleanBit . bitValue

En och noll

Representationen av numret 1 är uppenbarligen en typ med endast en konstruktör. I Haskell är denna typ kanoniskt typen () , kallad Enhet. Varje annan typ med endast en konstruktör är isomorf för () .

Och vår representation av 0 kommer att vara en typ utan konstruktörer. Detta är typen Void i Haskell, enligt definitionen i Data.Void . Detta skulle motsvara en obebodd typ utan datakonstruktörer:

data Void

Tillsats och multiplikation

Tillägget och multiplikationen har ekvivalenter i den här typen algebra. De motsvarar de taggade fackföreningarna och produkttyperna .

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

Vi kan se hur antalet invånare av alla slag motsvarar operationen i algebra.

På samma sätt kan vi använda Either och (,) som typkonstruktörer för tillägg och multiplikation. De är isomorfa för våra tidigare definierade typer:

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

De förväntade resultaten av tillsats och multiplikation följs av typen algebra fram till isomorfism. Vi kan till exempel se en isomorfism mellan 1 + 2, 2 + 1 och 3; som 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

Regler för tillägg och multiplikation

De vanliga reglerna för kommutativitet, associativitet och distribution är giltiga eftersom det finns triviala isomorfismer mellan följande typer:

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

Rekursiva typer

listor

Listor kan definieras som:

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

Om vi översätter detta till vår typ algebra, får vi

Lista (a) = 1 + a * Lista (a)

Men vi kan nu ersätta Lista (a) igen i detta uttryck flera gånger för att få:

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

Det är meningsfullt om vi ser en lista som en typ som bara kan innehålla ett värde, som i [] ; eller varje värde av typ a , som i [x] ; eller två värden av typ a , som i [x,y] ; och så vidare. Den teoretiska definitionen av lista som vi borde få därifrån skulle vara:

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

träd

Vi kan göra samma sak med till exempel binära träd. Om vi definierar dem som:

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

Vi får uttrycket:

Träd (a) = 1 + a * Träd (a) * Träd (a)

Och om vi gör samma ersättningar om och om igen, skulle vi få följande sekvens:

Träd (a) = 1 + a + 2 (a * a) + 5 (a * a * a) + 14 (a * a * a * a) + ...

Koefficienterna vi får här motsvarar den katalanska nummersekvensen, och det n: e katalanska antalet är exakt antalet möjliga binära träd med n-noder.

derivat

Derivatet av en typ är typen av dess typ av ett-håls sammanhang. Detta är den typen som vi skulle få om vi får en typvariabel att försvinna i alla möjliga punkter och summera resultaten.

Som exempel kan vi ta trippeltypen (a,a,a) och härleda den genom att få

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

Detta överensstämmer med vår vanliga definition av härledning, som:

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

Mer om detta ämne kan läsas i den här artikeln .

funktioner

Funktioner kan ses som exponentialer i vår algebra. Som vi ser, om vi tar en typ a med n instanser och en typ b med m instanser, kommer typen a -> b att ha m till kraften i n instanser.

Som ett exempel är Bool -> Bool isomorf för (Bool,Bool) , som 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)