Haskell Language
Tipo algebra

Números naturales en tipo álgebra

Podemos dibujar una conexión entre los tipos de Haskell y los números naturales. Esta conexión se puede hacer asignando a cada tipo el número de habitantes que tiene.

Tipos de union finita

Para tipos finitos, basta con ver que podemos asignar un tipo natural a cada número, basado en el número de constructores. Por ejemplo:

type Color = Red | Yellow | Green

sería 3 . Y el tipo Bool sería 2 .

type Bool = True | False

Unicidad hasta el isomorfismo

Hemos visto que múltiples tipos corresponderían a un solo número, pero en este caso, serían isomorfos. Es decir, habría un par de morfismos f y g , cuya composición sería la identidad, conectando los dos tipos.

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

f . g == id == g . f

En este caso, diríamos que los tipos son isomorfos . Consideraremos dos tipos iguales en nuestro álgebra siempre que sean isomorfos.

Por ejemplo, dos representaciones diferentes del número dos son trivalmente isomorfas:

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

Porque podemos ver bitValue . booleanBit == id == booleanBit . bitValue

Uno y cero

La representación del número 1 es obviamente un tipo con un solo constructor. En Haskell, este tipo es canónicamente el tipo () , llamado Unidad. Cada otro tipo con un solo constructor es isomorfo a () .

Y nuestra representación de 0 será un tipo sin constructores. Este es el tipo Void en Haskell, como se define en Data.Void . Esto sería equivalente a un tipo deshabitado, sin constructores de datos:

data Void

Suma y multiplicación

La suma y multiplicación tienen equivalentes en este tipo de álgebra. Se corresponden con las uniones etiquetadas y tipos de producto .

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

Podemos ver cómo el número de habitantes de cada tipo corresponde a las operaciones del álgebra.

De manera equivalente, podemos usar Either y (,) como constructores de tipo para la suma y la multiplicación. Son isomorfos a nuestros tipos previamente definidos:

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

Los resultados esperados de la suma y la multiplicación son seguidos por el tipo de álgebra hasta el isomorfismo. Por ejemplo, podemos ver un isomorfismo entre 1 + 2, 2 + 1 y 3; como 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

Reglas de suma y multiplicación.

Las reglas comunes de conmutatividad, asociatividad y distributividad son válidas porque existen isomorfismos triviales entre los siguientes tipos:

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

Tipos recursivos

Liza

Las listas se pueden definir como:

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

Si traducimos esto a nuestro tipo de álgebra, obtenemos

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

Pero ahora podemos sustituir la Lista (a) de nuevo en esta expresión varias veces, para obtener:

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

Esto tiene sentido si vemos una lista como un tipo que puede contener solo un valor, como en [] ; o cada valor de tipo a , como en [x] ; o dos valores de tipo a , como en [x,y] ; y así. La definición teórica de Lista que deberíamos obtener de allí sería:

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

Arboles

Podemos hacer lo mismo con árboles binarios, por ejemplo. Si los definimos como:

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

Obtenemos la expresión:

Árbol (a) = 1 + a * Árbol (a) * Árbol (a)

Y si hacemos las mismas sustituciones una y otra vez, obtendríamos la siguiente secuencia:

Árbol (a) = 1 + a + 2 (a * a) + 5 (a * a * a) + 14 (a * a * a * a) + ...

Los coeficientes que obtenemos aquí corresponden a la secuencia de números catalanes, y el número catalan n-th es precisamente el número de árboles binarios posibles con n nodos.

Derivados

La derivada de un tipo es el tipo de su tipo de contextos de un agujero. Este es el tipo que obtendríamos si hacemos que una variable de tipo desaparezca en cada punto posible y sumemos los resultados.

Como ejemplo, podemos tomar el tipo triple (a,a,a) , y derivarlo, obteniendo

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

Esto es coherente con nuestra definición habitual de derivación, como:

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

Más sobre este tema se puede leer en este artículo .

Funciones

Las funciones pueden verse como exponenciales en nuestro álgebra. Como podemos ver, si tomamos un tipo a con n instancias y un tipo b con m instancias, el tipo a -> b tendrá m para el poder de n instancias.

Como ejemplo, Bool -> Bool es isomorfo a (Bool,Bool) , como 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)