Haskell Language
Categoria teoria

La teoría de la categoría como sistema de organización de la abstracción.

La teoría de categorías es una teoría matemática moderna y una rama del álgebra abstracta centrada en la naturaleza de la conexión y la relación. Es útil para proporcionar bases sólidas y lenguaje común a muchas abstracciones de programación altamente reutilizables. Haskell utiliza la teoría de categorías como inspiración para algunas de las clases de tipos principales disponibles tanto en la biblioteca estándar como en varias bibliotecas populares de terceros.

Un ejemplo

La clase de tipos de Functor dice que si un tipo F crea una instancia de Functor (para el cual escribimos el Functor F ), entonces tenemos una operación genérica

fmap :: (a -> b) -> (F a -> F b)

lo que nos permite "mapear" sobre F . La intuición estándar (pero imperfecta) es que F a es un contenedor lleno de valores de tipo a y fmap nos permite aplicar una transformación a cada uno de estos elementos contenidos. Un ejemplo es Maybe

instance Functor Maybe where
  fmap f Nothing = Nothing     -- if there are no values contained, do nothing
  fmap f (Just a) = Just (f a) -- else, apply our transformation

Dada esta intuición, una pregunta común es "¿por qué no llamar a Functor algo obvio como Mappable ?".

Un indicio de la teoría de la categoría.

La razón es que Functor se ajusta a un conjunto de estructuras comunes en la teoría de categorías y, por lo tanto, al llamar a Functor "Functor" podemos ver cómo se conecta con este cuerpo de conocimiento más profundo.

En particular, la teoría de categorías está muy preocupada por la idea de las flechas de un lugar a otro. En Haskell, el conjunto de flechas más importante son las flechas de función a -> b . Una cosa común de estudiar en la teoría de categorías es cómo un conjunto de flechas se relaciona con otro conjunto. En particular, para cualquier constructor de tipo F , el conjunto de flechas de la forma F a -> F b también son interesantes.

Por lo que un Functor es cualquier F tal que existe una conexión entre Haskell normales flechas a -> b y el F flechas específicos de F a -> F b . La conexión está definida por fmap y también reconocemos algunas leyes que deben fmap

forall (x :: F a) . fmap id x == x

forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)

Todas estas leyes surgen naturalmente de la interpretación teórica de la categoría de Functor y no serían tan obviamente necesarias si solo Functor en Functor como relacionado con "mapear sobre elementos".

Definición de una categoría

Una categoría C consiste en:

• Una colección de objetos llamados Obj(C) ;
• Una colección (llamada Hom(C) ) de morfismos entre esos objetos. Si a y b son en Obj(C) , entonces un morfismo f en Hom(C) es típicamente denota f : a -> b , y la colección de todos morfismo entre a y b se denota hom(a,b) ;
• Un morfismo especial denominado morfismo de identidad : para cada a : Obj(C) existe un id : a -> a morfismo id : a -> a ;
• Un operador de composición ( . ), Tomando dos morfismos f : a -> b , g : b -> c produciendo un morfismo a -> c

que obedecen las siguientes leyes:

For all f : a -> x, g : x -> b, then id . f = f and g . id = g

For all f : a -> b, g : b -> c and h : c -> d, then h . (g . f) = (h . g) . f

En otras palabras, la composición con el morfismo de identidad (a la izquierda o a la derecha) no cambia el otro morfismo, y la composición es asociativa.

En Haskell, la Category se define como una clase de tipo en Control.Category :

-- | A class for categories.
--   id and (.) must form a monoid.
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

En este caso, cat :: k -> k -> * objetiva la relación de morfismo: existe un morfismo cat ab si y solo si cat ab está habitado (es decir, tiene un valor). a , b y c son todos en Obj(C) . Obj(C) sí está representado por el tipo k ; por ejemplo, cuando k ~ * , como suele ser el caso, los objetos son tipos.

El ejemplo canónico de una categoría en Haskell es la categoría de función:

instance Category (->) where
  id = Prelude.id
  (.) = Prelude..

Otro ejemplo común es la Category de flechas Kleisli para una Monad :

newtype Kleisli m a b = Kleisli (a -> m b)

class Monad m => Category (Kleisli m) where
  id = Kleisli return
  Kleisli f . Kleisli g = Kleisli (f >=> g)

Haskell tipifica como categoría

Definición de la categoría

Los tipos Haskell junto con las funciones entre tipos forman (casi †) una categoría. Tenemos un morfismo de identidad (función) ( id :: a -> a ) para cada objeto (tipo) a ; y composición de los morfismos ( (.) :: (b -> c) -> (a -> b) -> a -> c ), que obedecen a las leyes de categoría:

f . id = f = id . f
h . (g . f) = (h . g) . f 

Normalmente llamamos a esta categoría Hask .

Isomorfismos

En la teoría de categorías, tenemos un isomorfismo cuando tenemos un morfismo que tiene un inverso, en otras palabras, hay un morfismo que se puede componer con él para crear la identidad. En Hask esto equivale a tener un par de morfismos f , g tales que:

 f . g == id == g . f

Si encontramos un par de tales morfismos entre dos tipos, los llamamos isomorfos entre sí .

Un ejemplo de dos tipos isomorfos sería ((),a) y a para algunos a . Podemos construir los dos morfismos:

f :: ((),a) -> a
f ((),x) = x

g :: a -> ((),a)
g x = ((),x)

Y podemos comprobar que f . g == id == g . f .

Functores

Un funtor, en la teoría de categorías, va de una categoría a otra, mapeando objetos y morfismos. Estamos trabajando solo en una categoría, la categoría Hask of Haskell, por lo que vamos a ver solo los funtores de Hask a Hask , esos funtores, cuyos orígenes y categorías de destino son los mismos, se denominan endofunctores . Nuestros endofunctores serán los tipos polimórficos que toman un tipo y devuelven otro:

F :: * -> *

Obedecer las leyes de los funtores categóricos (preservar identidades y composición) es equivalente a obedecer las leyes de los funtores de Haskell:

fmap (f . g) = (fmap f) . (fmap g)
fmap id = id

Entonces, tenemos, por ejemplo, que [] , Maybe o (-> r) son funtores en Hask .

Mónadas

Una mónada en la teoría de categorías es un monoide en la categoría de endofunctores . Esta categoría tiene endofunctores como objetos F :: * -> * y transformaciones naturales (transformaciones entre ellos para todos forall a . F a -> G a ) como morfismos.

Un objeto monoide se puede definir en una categoría monoidal, y es un tipo que tiene dos morfismos:

zero :: () -> M
mappend :: (M,M) -> M

Podemos traducir esto aproximadamente a la categoría de endofunctores de Hask como:

return :: a -> m a
join :: m (m a) -> m a 

Y, obedecer las leyes de la mónada es equivalente a obedecer las leyes categóricas de los objetos monoides.

† De hecho, la clase de todos los tipos junto con la clase de funciones entre los tipos no forman estrictamente una categoría en Haskell, debido a la existencia de undefined . Por lo general, esto se soluciona simplemente definiendo los objetos de la categoría Hask como tipos sin valores inferiores, que excluyen funciones no terminadas y valores infinitos (codata). Para una discusión detallada de este tema, vea aquí .

Producto de tipos en Hask.

Productos categoricos

En la teoría de categorías, el producto de dos objetos X , Y es otro objeto Z con dos proyecciones: π₁: Z → X y π₂: Z → Y ; de tal manera que cualquier otro dos morfismos de otro objeto se descomponga de forma única a través de esas proyecciones. En otras palabras, si existe f₁: W → X y f₂: W → Y , existe un morfismo único g: W → Z tal que π₁ ○ g = f₁ y π₂ ○ g = f₂ .

Productos en Hask

Esto se traduce en la categoría Hask de tipos de Haskell como sigue, Z es producto de A , B cuando:

-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g  :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2

El tipo de producto de dos tipos A , B , que sigue la ley mencionada anteriormente, es la tupla de los dos tipos (A,B) , y las dos proyecciones son fst y snd . Podemos verificar que sigue la regla anterior, si tenemos dos funciones f1 :: W -> A y f2 :: W -> B , podemos descomponerlas de forma única de la siguiente manera:

decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))

Y podemos comprobar que la descomposición es correcta:

fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2

Unicidad hasta el isomorfismo

La elección de (A,B) como el producto de A y B no es única. Otra opción lógica y equivalente habría sido:

data Pair a b = Pair a b

Además, podríamos haber elegido (B,A) como el producto, o incluso (B,A,()) , y podríamos encontrar una función de descomposición como la anterior también siguiendo las reglas:

decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))

Esto se debe a que el producto no es único, sino único hasta isomorfismo . Cada dos productos de A y B no tienen que ser iguales, pero deben ser isomorfos. Como ejemplo, los dos productos diferentes que acabamos de definir, (A,B) y (B,A,()) , son isomorfos:

iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())

iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)

Singularidad de la descomposición.

Es importante señalar que también la función de descomposición debe ser única. Hay tipos que siguen todas las reglas requeridas para ser producto, pero la descomposición no es única. Como ejemplo, podemos tratar de usar (A,(B,Bool)) con proyecciones fst fst . snd como producto de A y B :

decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))

Podemos comprobar que funciona:

fst         . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x

Pero el problema aquí es que podríamos haber escrito otra descomposición, a saber:

decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))

Y, como la descomposición no es única , (A,(B,Bool)) no es el producto de A y B en Hask

Coproducto de tipos en Hask

Intuición

El producto categórico de dos tipos A y B debe contener la información mínima necesaria para contener dentro de una instancia de tipo A o tipo B. Podemos ver ahora que el coproducto intuitivo de dos tipos debe ser Either ab . Otros candidatos, como Either a (b,Bool) , contendrían una parte de información innecesaria y no serían mínimos.

La definición formal se deriva de la definición categórica de coproducto.

Coproductos categóricos

Un coproducto categórico es la noción dual de un producto categórico. Se obtiene directamente invirtiendo todas las flechas en la definición del producto. El coproducto de dos objetos X , Y es otro objeto Z con dos inclusiones: i_1: X → Z e i_2: Y → Z ; de modo que cualquier otro dos morfismos de X e Y a otro objeto se descomponen de forma única a través de esas inclusiones. En otras palabras, si hay dos morfismos f₁: X → W y f₂: Y → W , existe un morfismo único g: Z → W tal que g ○ i₁ = f₁ y g ○ i₂ = f₂

Coproductos en Hask

La traducción a la categoría de Hask es similar a la traducción del producto:

-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g  :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2

El tipo coproducto de dos tipos A y B en Hask es Either ab o cualquier otro tipo isomorfo a la misma:

-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b

-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x)  = f1 x
decompose f1 f2 (Right y) = f2 y 

Haskell Applicative en términos de la teoría de la categoría

El Functor de Haskell permite asignar cualquier tipo a (un objeto de Hask ) a un tipo F a y también asignar una función a -> b (un morfismo de Hask ) a una función con el tipo F a -> F b . Esto corresponde a una definición de teoría de categorías en un sentido en que el funtor conserva la estructura básica de categorías.

Una categoría monoidal es una categoría que tiene alguna estructura adicional :

• Un producto tensorial (ver Producto de tipos en Hask )
• Una unidad tensorial (objeto unitario)

Tomando un par como nuestro producto, esta definición se puede traducir a Haskell de la siguiente manera:

class Functor f => Monoidal f where
    mcat :: f a -> f b -> f (a,b)
    munit :: f ()

La clase Applicative es equivalente a esta Monoidal y, por lo tanto, puede implementarse en términos de esta:

instance Monoidal f => Applicative f where
    pure x = fmap (const x) munit
    f <*> fa = (\(f, a) -> f a) <$> (mcat f fa)