El type system tiene un type system

En el post anterior presenté type constructors, kinds y higher-kinded types desde la sintaxis de Scala 3. Aquel texto estaba deliberadamente pegado al código: aquí está el concepto, aquí está cómo se escribe, aquí está por qué al compilador le importa.

Este post baja un nivel más. Los conceptos detrás de F[_] no nacieron en la programación. Vienen de la category theory, y la relación entre ambos mundos no es una metáfora bonita ni una analogía de sobremesa. Es una correspondencia estructural. Los type constructors son functors. Las funciones polimórficas son natural transformations. Los kinds son un simply-typed lambda calculus un nivel más arriba. Y el parametric polymorphism te regala las condiciones de naturalidad sin que tengas que demostrarlas a mano.

Si has leído Sintaxis y Semántica 3 o el post de tagless final, probablemente ya tengas la intuición. Lo que sigue intenta hacerla precisa sin perder del todo la respiración humana en el camino.

La categoría que fingimos que existe

#

Antes de hablar de functors, hay que fijar el escenario. En programación, el candidato habitual es Hask: la categoría donde los objetos son tipos y los morfismos son funciones.

Hasta aquí, todo suena razonable. Las leyes categoriales que nos interesan, como la asociatividad de la composición o la identidad como elemento neutro, se cumplen para funciones puras. Pero en cuanto intentas ser completamente riguroso aparece la primera grieta: Hask no es técnicamente una categoría en sentido estricto. Andrej Bauer demostró en 2016 que la presencia de bottom values (???, no-terminación, null) rompe la ley de identidad. En Haskell, seq puede distinguir undefined de undefined . id, violando f . id = f.

La salida práctica, y también la más honesta para este contexto, es trabajar en lo que suele llamarse “Platonic Hask”: el fragmento total donde toda computación termina y no existen bottom values. En ese fragmento, las leyes vuelven a encajar y las intuiciones que usamos los programadores funcionales son correctas. En el resto del post, cuando diga Hask, me refiero a eso.

Los type constructors son endofunctors

#

Con el escenario ya fijado, podemos hablar de functors. Un functor F: C -> D entre dos categorías mapea objetos a objetos y morfismos a morfismos, preservando identidad y composición:

• Object mapping: Para cada objeto A en C, un objeto F(A) en D
• Morphism mapping: Para cada morfismo f: A -> B, un morfismo F(f): F(A) -> F(B)
• Leyes: F(id) = id, y F(g . f) = F(g) . F(f)

Cuando C y D son la misma categoría, F recibe el nombre de endofunctor.

List es el ejemplo más familiar. Es un endofunctor en Hask. El object mapping es el propio type constructor: List mapea el tipo Int al tipo List[Int]. El morphism mapping es map: dado f: A => B, obtienes List[A] => List[B].

trait Functor[F[_]]:
  extension [A](fa: F[A])
    def map[B](f: A => B): F[B]

Las leyes del functor, vistas desde código, se traducen de forma casi literal:

// Identidad: hacer map con identity no hace nada
xs.map(identity) == xs

// Composición: hacer map de una composición equivale a componer los maps
xs.map(f andThen g) == xs.map(f).map(g)

Aquí aparece una de esas correspondencias que conviene tomarse en serio. La type class Functor[F[_]] certifica que F es un endofunctor en Hask. La sintaxis F[_] exige que F tenga kind * -> *, que es exactamente lo que significa “endofunctor en Hask”: un mapeo de tipos a tipos.

Las funciones polimórficas son natural transformations

#

El siguiente paso natural es preguntarse qué corresponde, en category theory, a una función polimórfica entre dos type constructors. La respuesta es una natural transformation. Una natural transformation alpha: F => G entre dos functors F, G: C -> C es una familia de morfismos, uno por cada objeto A:

alpha_A : F(A) -> G(A)

que satisface la condición de naturalidad: para cada morfismo f: A -> B,

G(f) . alpha_A  =  alpha_B . F(f)

Dibujado como un diagrama conmutativo:

        alpha_A
 F(A) ---------> G(A)
  |                |
  | F(f)           | G(f)
  |                |
  v                v
 F(B) ---------> G(B)
        alpha_B

La intuición del diagrama es sencilla: da igual por qué lado recorras el cuadrado, el resultado debe coincidir.

En Scala, headOption sirve como ejemplo muy legible de natural transformation de List a Option:

def headOption[A](xs: List[A]): Option[A] = xs.headOption

La condición de naturalidad dice:

// Estos deben ser iguales para todo f: A => B
list.map(f).headOption  ==  list.headOption.map(f)

No importa si primero transformas los elementos y luego extraes la cabeza, o si haces esas dos cosas en el orden contrario. La natural transformation conmuta con el map del functor. Esa es, en el fondo, toda la idea.

Se pueden codificar natural transformations explícitamente en Scala 3:

// FunctionK: una natural transformation de F a G
trait ~>[F[_], G[_]]:
  def apply[A](fa: F[A]): G[A]

val headOpt: List ~> Option = new (List ~> Option):
  def apply[A](fa: List[A]): Option[A] = fa.headOption

O usando los polymorphic function types de Scala 3:

val headOpt: [A] => List[A] => Option[A] =
  [A] => (xs: List[A]) => xs.headOption

Parametricity te da naturalidad gratis

#

Aquí aparece uno de los puntos más bonitos de todo este tema. En category theory general, la condición de naturalidad hay que demostrarla para cada natural transformation. En Hask, normalmente no hace falta. El parametric polymorphism lo hace por ti.

Philip Wadler mostró en 1989 que la firma de tipos de una función parametrically polymorphic, por sí sola, ya implica un teorema que cualquier implementación debe satisfacer. Su técnica traduce tipos a relaciones: el free theorem para una función polimórfica entre functors es exactamente su condición de naturalidad.

Para cualquier función r: [A] => List[A] => List[A], el free theorem es:

r(list.map(f)) == r(list).map(f)

Esto se cumple porque r no puede inspeccionar ni fabricar valores de tipo A. Lo único que puede hacer es reorganizar, descartar o duplicar posiciones de la lista. La parametricity, es decir, la imposibilidad de examinar un type parameter como si supieras de qué tipo concreto se trata, fuerza el mismo comportamiento estructural sin importar qué elementos haya dentro. Y eso es, precisamente, lo que la naturalidad exige.

La conexión profunda queda entonces bastante limpia: en un lenguaje con parametric polymorphism, toda función polimórfica entre functors es automáticamente una natural transformation. La naturalidad sale gratis.

Los kinds como lambda calculus a nivel de tipos

#

Hasta aquí hemos hablado de type constructors como si fueran funciones sobre tipos. Ahora toca justificar esa intuición con un poco más de precisión. Mark P. Jones formalizó esto en su paper de 1995 sobre constructor classes. El kind system es un simply-typed lambda calculus a nivel de tipos:

k ::= *           -- proper types (tipo base)
    | k1 -> k2    -- type constructors (tipo función)

Esto refleja exactamente la gramática del simply-typed lambda calculus (STLC):

tau ::= Base       -- tipo base
      | tau -> tau  -- tipo función

La estructura es la misma. Igual que el STLC tiene variables a nivel de términos, abstracción y aplicación, el kind system tiene variables a nivel de tipos, type abstraction (type lambdas en Scala 3) y type application (aplicar un type constructor a un argumento).

Scala 3 hace las type lambdas explícitas:

// Una type lambda: aplicar parcialmente Either, fijando la izquierda a String
type StringOr = [X] =>> Either[String, X]
// StringOr tiene kind * -> *

// Esto permite usar Either (kind * -> * -> *) donde se espera * -> *
given Functor[StringOr] with
  extension [A](e: Either[String, A])
    def map[B](f: A => B): Either[String, B] = e.map(f)

Mirado así, [X] =>> Either[String, X] no es solo una sintaxis curiosa de Scala 3. Es lambda abstraction a nivel de tipos. Y StringOr[Int] es type application, que produce Either[String, Int].

El kind polymorphism (AnyKind en Scala 3, PolyKinds en Haskell) va un paso más allá: permite que un type parameter cubra todos los kinds, no solo *. Eso resulta útil para type-level tags y phantom types que deben funcionar en cualquier kind.

El Yoneda lemma, brevemente

#

Con esto en su sitio, podemos asomarnos a una de las piezas más famosas de category theory. El Yoneda lemma es uno de sus resultados centrales. Para un functor F: C -> Set y un objeto A en C:

Nat(Hom(A, -), F) ≅ F(A)

El conjunto de natural transformations del representable functor Hom(A, -) a F es isomorfo al conjunto F(A).

En Scala, esa idea aparece como Yoneda encoding:

// Yoneda[F, A] ≅ F[A]
trait Yoneda[F[_], A]:
  def apply[B](f: A => B): F[B]

def toYoneda[F[_]: Functor, A](fa: F[A]): Yoneda[F, A] =
  new Yoneda[F, A]:
    def apply[B](f: A => B): F[B] = fa.map(f)

def fromYoneda[F[_], A](y: Yoneda[F, A]): F[A] =
  y.apply(identity)

La consecuencia práctica es menos abstracta de lo que parece. Yoneda[F, A] fusiona cadenas de map. Cuando encadenas y.map(f).map(g).map(h), el Yoneda encoding lo reduce a un solo y.map(f andThen g andThen h) automáticamente, porque map sobre Yoneda no hace más que componer funciones. No aparecen estructuras intermedias.

La construcción dual, CoYoneda, te da un free functor: hace que cualquier type constructor, incluso uno sin instancia de Functor, se comporte como un functor. Esa idea está en la base de muchas implementaciones de free monads.

Después de todo este recorrido, conviene dejar la correspondencia resumida en una tabla.

La tabla de correspondencia

#

Referencias

#

• Mark P. Jones, “A system of constructor classes: overloading and implicit higher-order polymorphism”, Journal of Functional Programming 5(1), 1995. El paper que introdujo los kinds en el type class system de Haskell e hizo posibles Functor, Monad, etc. como constructor classes.

• Philip Wadler, “Theorems for free!”, FPCA ‘89, 1989. Demuestra que la firma de tipos de una función parametrically polymorphic implica un teorema (el “free theorem”) que cualquier implementación debe satisfacer. Para funciones entre functors, el free theorem es la condición de naturalidad.

• Andrej Bauer, “Hask is not a category”, 2016. Un argumento riguroso de que los bottom values y seq rompen las leyes categoriales en Haskell. La respuesta pragmática es trabajar en “Platonic Hask” donde toda computación termina.

• Bartosz Milewski, Category Theory for Programmers, 2018. Capítulos sobre functors, natural transformations y el Yoneda lemma, escritos para programadores con ejemplos en Haskell y C++. Existe una edición adaptada a Scala.

• Documentación de Scala 3: Type Lambdas, Kind Polymorphism. La referencia oficial para el kind system y la sintaxis de type lambdas en Scala 3.