Haskell Language
Digitare algebra

Numeri naturali in tipo algebra

Possiamo tracciare una connessione tra i tipi Haskell e i numeri naturali. Questa connessione può essere effettuata assegnando ad ogni tipo il numero di abitanti che ha.

Tipi di unione finiti

Per i tipi finiti, è sufficiente vedere che possiamo assegnare un tipo naturale a ogni numero, in base al numero di costruttori. Per esempio:

type Color = Red | Yellow | Green

sarebbe 3 . E il tipo Bool sarebbe 2 .

type Bool = True | False

Unicità fino all'isomorfismo

Abbiamo visto che più tipi corrisponderebbero a un singolo numero, ma in questo caso sarebbero isomorfi. Questo per dire che ci sarebbe una coppia di morfismi f e g , la cui composizione sarebbe l'identità, collegando i due tipi.

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

f . g == id == g . f

In questo caso, diremmo che i tipi sono isomorfi . Considereremo due tipi uguali nella nostra algebra fintanto che sono isomorfi.

Ad esempio, due diverse rappresentazioni del numero due sono banalmente isomorfiche:

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

Perché possiamo vedere bitValue . booleanBit == id == booleanBit . bitValue

Uno e zero

La rappresentazione del numero 1 è ovviamente un tipo con un solo costruttore. In Haskell, questo tipo è canonicamente il tipo () , chiamato Unità. Ogni altro tipo con un solo costruttore è isomorfo a () .

E la nostra rappresentazione di 0 sarà un tipo senza costruttori. Questo è il tipo Void in Haskell, come definito in Data.Void . Questo sarebbe equivalente a un tipo non modificato, senza costruttori di dati:

data Void

Aggiunta e moltiplicazione

L'addizione e la moltiplicazione hanno equivalenti in questo tipo di algebra. Corrispondono alle unioni e ai tipi di prodotto contrassegnati .

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

Possiamo vedere come il numero di abitanti di ogni tipo corrisponda alle operazioni dell'algebra.

Equivalentemente, possiamo usare Either e (,) come costruttori di tipi per l'addizione e la moltiplicazione. Sono isomorfi ai nostri tipi precedentemente definiti:

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

I risultati attesi di addizione e moltiplicazione sono seguiti dall'algebra di tipo fino all'isomorfismo. Ad esempio, possiamo vedere un isomorfismo tra 1 + 2, 2 + 1 e 3; come 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

Regole di addizione e moltiplicazione

Le regole comuni di commutatività, associatività e distributività sono valide perché ci sono isomorfismi banali tra i seguenti tipi:

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

Tipi ricorsivi

elenchi

Le liste possono essere definite come:

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

Se traduciamo questo nel nostro tipo di algebra, otteniamo

Elenco (a) = 1 + a * Elenco (a)

Ma ora possiamo sostituire List (a) in questa espressione più volte, per ottenere:

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

Questo ha senso se vediamo un elenco come un tipo che può contenere solo un valore, come in [] ; o ogni valore di tipo a , come in [x] ; o due valori di tipo a , come in [x,y] ; e così via. La definizione teorica di List che dovremmo ottenere da lì sarebbe:

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

Alberi

Per esempio, possiamo fare la stessa cosa con gli alberi binari. Se li definiamo come:

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

Otteniamo l'espressione:

Albero (a) = 1 + a * Albero (a) * Albero (a)

E se facciamo sempre le stesse sostituzioni, otterremmo la seguente sequenza:

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

I coefficienti che otteniamo qui corrispondono alla sequenza di numeri catalani, e il n-esimo numero catalano è precisamente il numero di possibili alberi binari con n nodi.

Derivati

La derivata di un tipo è il tipo del suo tipo di contesti a un buco. Questo è il tipo che otterremmo se facessimo sparire una variabile di tipo in ogni punto possibile e sommare i risultati.

Ad esempio, possiamo prendere il tipo triplo (a,a,a) , e derivarlo, ottenendo

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

Questo è coerente con la nostra usuale definizione di derivazione, come:

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

Maggiori informazioni su questo argomento possono essere lette su questo articolo .

funzioni

Le funzioni possono essere viste come esponenziali nella nostra algebra. Come possiamo vedere, se prendiamo un tipo a con n istanze e un tipo b con m istanze, il tipo a -> b avrà m al potere di n istanze.

Ad esempio, Bool -> Bool è isomorfo a (Bool,Bool) , come 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)