Capítulo 19 · Kinds: un catálogo de álgebras

Este capítulo paga una promesa que el §2.6 dejó abierta: en kaikai el tipo no es la única etiqueta, y las familias de etiquetas, los kinds, tienen un mecanismo común. Ya lo tocaste por partes. Cuando en el capítulo 10 escribiste fn promedio[u: Measure](...), u no era un parámetro de tipo común: no podía ser Int ni String ni ningún tipo, solo una unidad. Estabas cuantificando sobre otra familia de cosas, con otras reglas.

Y no hay una sola. Los tipos que unifica el inferidor, las filas de efectos de cada firma, las unidades que multiplican y cancelan, las monedas del stdlib, las regiones de memoria del runtime: cada una es un kind distinto, con su propia álgebra. kaikai los declara todos en un mismo lugar y con el mismo mecanismo, y aquí recorres ese catálogo completo.

Es el capítulo más abstracto del libro, y por eso va al final: no necesitas nada de esto para escribir kaikai productivo. Pero si llegaste hasta aquí, apuesto a que la pregunta ya te apareció sola: ¿qué tienen en común las unidades del capítulo 10, los efectos del 12 y la memoria del 13? La respuesta es corta y creo que elegante.

19.1 Qué es un kind

Un tipo clasifica valores: 42 habita Int, "hola" habita String. Un kind clasifica un peldaño más arriba: sus habitantes son símbolos que participan en los tipos. Int habita el kind Type. La unidad m habita el kind Measure. El efecto Stdout habita el kind Effect.

La consecuencia práctica la viste en el capítulo 10: un parámetro [u: Measure] solo acepta unidades, y el compilador razona sobre u con las reglas de las unidades: u^2 tiene sentido, u y kg unifican solo si son la misma. Un parámetro [t] corriente, en cambio, acepta tipos y se razona con las reglas de los tipos. La anotación de kind le dice al compilador qué álgebra usar para decidir si dos cosas son iguales.

Ese es todo el concepto: un kind es una familia de habitantes más el álgebra con que el compilador los unifica. A esa álgebra kaikai la llama theory.

19.2 Las theories: álgebras de unificación

Cuando el compilador ve Real<m * s> y Real<s * m>, ¿son el mismo tipo? Para responder necesita saber que el producto de unidades conmuta. Cuando ve dos filas de efectos Stdout + Fail y Fail + Stdout, necesita saber que el orden de una fila no importa. Cuando ve dos regiones r1 y r2, necesita saber que jamás son iguales salvo que sean literalmente la misma.

Cada una de esas preguntas se responde con una theory: un conjunto de reglas de ecuación que el compilador aplica al unificar habitantes de un kind. Tres cosas la definen:

• Es decidible. El algoritmo de unificación termina siempre, y rápido. No hay solver SMT ni búsqueda: son álgebras elegidas precisamente porque su unificación es un cálculo directo.
• Se borra en runtime. Igual que las unidades del capítulo 10: la theory decide en compilación qué programas son legales, y desaparece del binario.
• El catálogo es cerrado. Puedes declarar habitantes nuevos (unit parsec) y hasta kinds nuevos (§19.5), pero no una theory nueva: el compilador responde unknown theory. El §19.12 defiende por qué esa decisión de diseño es permanente.

19.3 El catálogo completo

El catálogo vive en stdlib/core/kinds.kai y es corto. Este es un extracto (el archivo real trae un comentario por entrada):

# fragmento de stdlib/core/kinds.kai
theory HindleyMilner  = builtin
theory EffectRow      = builtin
theory AbelianGroup   = { assoc, commut, inverse, identity }
theory Module         = { assoc, commut, inverse, identity }
theory Nominal        = builtin
theory ConstructorApp = builtin
theory Semilattice    = { assoc, commut, idempotent }
theory Composition    = { assoc, measure }

kind Type     : HindleyMilner  with type
kind Effect   : EffectRow      with effect
kind Measure  : AbelianGroup   with unit
kind Currency : Module over T  with currency
kind Region   : Nominal        with region
kind Perm     : Semilattice    with perm
kind Layout   : Composition over Int with layout { be le }
kind Dim      : HindleyMilner  with Int
kind Shape    : ConstructorApp

Cada kind nombra su theory y, tras el with, su palabra introductora: la declaración que acuña habitantes. type acuña habitantes de Type. effect acuña habitantes de Effect. unit acuña habitantes de Measure. Dos kinds no siguen ese molde: Shape no lleva with porque sus habitantes no se declaran, se derivan (cada type T[a] de un solo parámetro ya es uno), y Dim escribe with Int, lo que significa que sus habitantes son valores de Int (<3>, <128>), no símbolos acuñados. Llevas todo el libro acuñando habitantes de kinds; te faltaba el organigrama:

Kind	Theory	Introductor	Habitantes	Qué decide la theory
Type	HindleyMilner	type	Int, String, los tuyos	igualdad e inferencia de tipos
Effect	EffectRow	effect	Stdout, Cancel, los tuyos	filas: orden irrelevante, duplicados colapsan
Measure	AbelianGroup	unit	m, s, USD si quieres	producto, cociente y potencia de unidades
Currency	Module	currency	USD, EUR, … (stdlib/money.kai)	suma y escala; sin producto
Region	Nominal	region	uno fresco por bloque region	identidad: cada arena es solo ella misma
Perm	Semilattice	perm	read, write, los tuyos	unión idempotente; subsunción por el orden del retículo
Layout	Composition	layout	be, le	orden de bytes; asociativa, no conmutativa
Dim	HindleyMilner	with Int	<3>, <128>: valores Int	igualdad de índices: <3> ~ <3>, nunca <4>
Shape	ConstructorApp	(derivados)	List, Vec, Option, Tree[a]	aridad-1: List ~ List, nunca List ~ Vec

Cuatro theories dicen builtin: su motor es el compilador mismo. HindleyMilner es el inferidor de tipos que te acompaña desde el capítulo 3, y notarás que sirve a dos kinds, Type y Dim: una theory nombra un motor de unificación, y nada obliga a que un motor clasifique un solo kind. EffectRow es la unificación de filas del capítulo 12; Nominal es igualdad de símbolo, que el núcleo ya sabía hacer; ConstructorApp liga constructores de un argumento, y lo usas en §19.11. Las otras cuatro se describen por propiedades algebraicas. Dos se ven casi idénticas, AbelianGroup y Module, y la diferencia es sobre qué operación rigen sus propiedades. En AbelianGroup, los habitantes mismos forman un grupo bajo el producto: m * s, m^2, 1/s son habitantes nuevos derivados. En Module, la estructura es solo aditiva: las cantidades de un habitante se suman y se escalan por un número, pero los habitantes no se multiplican entre sí. USD^2 no es un habitante de Currency; no existe. Esa asimetría es deliberada y el §19.7 la explota. Semilattice es una unión idempotente sin inverso: los habitantes se juntan con + (read + write, y read + read = read), y nada se resta; unificar es subsunción por el orden del retículo, así que un permiso con más capacidades fluye donde se piden menos, nunca al revés. Y Composition es asociativa pero no conmutativa, porque el orden carga significado, y suma una medida por elemento (§19.8).

Nota lo que no está en la tabla: nada tuyo. El catálogo completo del lenguaje cabe en una pantalla: nueve kinds, ocho theories, y todo lo que llevas leído se construye sobre ellos.

19.4 Cuantificar sobre cualquier kind

Esto es un sistema, y no nueve features apiladas, porque la cuantificación funciona igual sobre cualquier kind. Compara estas tres firmas:

fn area_de[u: Measure](ancho: Real<u>, alto: Real<u>) : Real<u^2>
fn insertar[r: Region](t: Arbol<r>, k: Int) : Arbol<r>
pub fn convert[a: Currency, b: Currency](m: Money[dec.Decimal]<a>, rate: dec.Decimal) : Money[dec.Decimal]<b>

La primera la escribiste en el capítulo 10. La segunda la escribes en el §19.6. La tercera viene tal cual de stdlib/money.kai. Las tres dicen lo mismo: “para cualquier habitante de este kind”. Y en las tres, el compilador aplica la theory del kind al verificar el cuerpo: en area_de puede formar u^2 porque AbelianGroup tiene producto; en insertar exige que el árbol que entra y el que sale vivan en la misma región porque Nominal no unifica regiones distintas; en convert permite que a y b difieran porque son dos parámetros: la puerta explícita entre monedas del capítulo 10, ahora con su mecanismo a la vista.

El listado 19.1 es la primera firma, completa y corriendo:

# Listado 19.1: ejemplos/cap19/01_generica_sobre_unidades.kai
unit m
unit s

fn area_de[u: Measure](ancho: Real<u>, alto: Real<u>) : Real<u^2> =
  ancho * alto

fn main() : Unit / Stdout {
  let a1 = area_de(3.0<m>, 4.0<m>)      # Real<m^2>
  let a2 = area_de(3.0<s>, 4.0<s>)      # Real<s^2>
  println("#{a1}")
  println("#{a2}")
}

$ kai run ejemplos/cap19/01_generica_sobre_unidades.kai
12 m^2
12 s^2

Fíjate en la salida: el Show de un Real con unidad imprime la unidad, potencia incluida. “Segundos al cuadrado” es una unidad rara en la física de este mundo, pero el álgebra no opina de física: opina de consistencia.

19.5 Kinds propios

Measure no es especial. Tú también puedes usar la declaración kind, con las cuatro theories no-builtin como opciones. Rinde, por ejemplo, para separar sistemas de unidades que jamás deben mezclarse, ni siquiera con una conversión accidental.

# Listado 19.2: ejemplos/cap19/02_kind_propio.kai
kind Metrica  : AbelianGroup with metrica
kind Imperial : AbelianGroup with imperial

metrica m
metrica s
imperial ft

fn velocidad(d: Real<m>, t: Real<s>) : Real<m/s> = d / t

fn main() : Unit / Stdout {
  let v = velocidad(100.0<m>, 10.0<s>)
  println("#{v}")

  # Esto no compila: m vive en Metrica, ft vive en Imperial.
  #   fn mala(a: Real<m>, b: Real<ft>) : Real<m> = a + b
}

$ kai run ejemplos/cap19/02_kind_propio.kai
10 m/s

Cada kind ... with palabra acuña también su propia palabra introductora: aquí metrica y imperial declaran habitantes igual que unit lo hace para Measure. Dos habitantes de kinds distintos nunca unifican, aunque ambos midan longitud. En el capítulo 10, m + ft era un error de unidades; aquí el error es más profundo: no hay un álgebra común donde plantear la pregunta. Es la clase de bug del Mars Climate Orbiter, libras-fuerza leídas como newtons, y aquí la cierra una frontera de kinds en vez de una convención de nombres.

Los kinds aditivos también se pueden declarar (kind Puntos : Module with puntos): sirven para cantidades que se suman y escalan pero donde “puntos al cuadrado” sería un sinsentido: puntos de un juego, millas de viajero, créditos académicos. Las cuatro theories builtin no aceptan kinds de usuario: si escribes kind Zona : Nominal, el compilador te dice que una theory builtin no puede clasificar un kind tuyo. Las regiones, los tipos, los efectos y las formas tienen exactamente un kind cada uno, y es del lenguaje.

19.6 Region: memoria como habitante

El capítulo 13 te debe una. Ahí aprendiste que Perceus inserta increments y decrements en los puntos exactos donde los valores mueren, y quedó una pregunta abierta: ¿y si un cálculo construye un millón de valores efímeros solo para plegarlos a un número? Cada celda lleva su alta y su baja en el contador, y un humano que mira el programa sabe que todo ese contabilismo sobra: nada de esto sobrevive al cálculo.

El bloque region se lo dice al compilador:

# Listado 19.3: ejemplos/cap19/03_region_scratch.kai
fn suma(xs: [Int]) : Int = match xs {
  []        -> 0
  [h, ...t] -> h + suma(t)
}

fn main() : Unit / Stdout {
  let total = region {
    let a = [1, 2, 3, 4, 5]        # construida en la arena
    let b = [10, 20, 30]           # construida en la arena
    suma(a) + suma(b)              # resultado escalar
  }                                # la arena se libera aquí, de un golpe
  println("#{total}")
}

$ kai run ejemplos/cap19/03_region_scratch.kai
75

Todo constructor escrito léxicamente dentro del bloque asigna en una arena: un bloque de memoria que crece por bump (un puntero que avanza, sin contador alguno) y se libera entero al cerrar la llave. Las dos listas de arriba no llevan ni un increment ni un decrement, y el escalar que sale cruza la frontera gratis.

¿Y si necesitas que la estructura cruce funciones antes de plegarse? Ahí aparece el kind. La forma region { r -> ... } liga un nombre para la región, y ese r es un habitante fresco de Region que los tipos pueden cargar:

# Listado 19.4: ejemplos/cap19/04_arbol_en_arena.kai
type Arbol = Hoja | Nodo(Arbol, Int, Arbol)

fn insertar[r: Region](t: Arbol<r>, k: Int) : Arbol<r> =
  match t {
    Hoja -> Nodo(Hoja, k, Hoja)
    Nodo(izq, v, der) ->
      if k < v { Nodo(insertar(izq, k), v, der) }
      else if k > v { Nodo(izq, v, insertar(der, k)) }
      else { Nodo(izq, v, der) }
  }

fn sumar[r: Region](t: Arbol<r>) : Int =
  match t {
    Hoja -> 0
    Nodo(izq, v, der) -> sumar(izq) + v + sumar(der)
  }

fn construir[r: Region](t: Arbol<r>, n: Int) : Arbol<r> =
  if n == 0 { t } else { construir(insertar(t, n), n - 1) }

fn main() : Unit / Stdout {
  let total = region { r ->
    let arbol = construir(Hoja, 100)
    sumar(arbol)
  }                                # 100 nodos liberados de un golpe
  println("#{total}")
}

$ kai run ejemplos/cap19/04_arbol_en_arena.kai
5050

Mira las firmas con los ojos del §19.4: insertar es genérica sobre la región exactamente como area_de es genérica sobre la unidad. Arbol<r> marca en el tipo que estos nodos viven en la arena r; el tipo Arbol se declara una sola vez, sin saber nada de regiones, y cualquier función puede volverse region-polimórfica anotando [r: Region]. Cien nodos, cero operaciones de contador, una liberación.

La theory Nominal es la más simple del catálogo: cada bloque region { r -> } acuña un habitante fresco, distinto de todos los demás, y dos regiones no unifican jamás. Eso impide que un Arbol<r1> se cuele en una arena r2 que se libera en otro momento: el error es de tipos, en compilación, con el mismo mecanismo que rechaza m + ft.

Dos letras chicas, las dos importantes:

• Lo que escapa se copia. El valor del bloque cruza la frontera: si es un escalar, gratis; si es una estructura, se copia en profundidad a la memoria normal con RC antes de liberar la arena. Una región cuyo resultado es la estructura entera es más lenta que no usar región. El nicho es scratch que se pliega a poco.
• La arena es léxica en la forma sin nombre. En region { ... } sin binder, solo los constructores escritos dentro del bloque asignan en la arena; un helper llamado desde el bloque asigna en la memoria normal. Para cruzar funciones, usa el binder y firmas [r: Region], como en el listado 19.4.

region es opt-in: el compilador nunca lo infiere por ti. Por omisión, la memoria sigue siendo la del capítulo 13: Perceus, exacto y sin pausas. region es la palanca que tiras cuando el perfil te muestra un cálculo que construye y descarta a paladas.

19.7 Dinero: el álgebra que falta a propósito

En el capítulo 10 modelaste monedas con unit USD, y funciona. Pero queda abierta una puerta curiosa: en Measure, los habitantes forman grupo bajo producto, así que USD^2 y USD*EUR son unidades perfectamente formables. Ningún programa contable sensato las produce a propósito, pero un bug sí puede, y el sistema de tipos las aceptaría con la solemnidad con que acepta m/s^2.

Para dinero, el stdlib usa el kind Currency, cuya theory Module simplemente no tiene producto de habitantes. El tipo es Money[t]<c>: un carrier t (el tipo que guarda el monto) etiquetado con la moneda c en la ranura <>. Para dinero de verdad el carrier es Decimal, aritmética exacta de punto fijo y no punto flotante, que es lo único defendible. Casi siempre escribes Money[Decimal]<USD>:

# Listado 19.5: ejemplos/cap19/05_dinero.kai
import money
import decimal as dec

fn main() : Unit / Stdout {
  let a: Money[dec.Decimal]<USD> = 10.50<USD>
  let b: Money[dec.Decimal]<USD> = 4.50<USD>
  let total = a + b                       # misma moneda: Money[Decimal]<USD>

  let k: dec.Decimal = 3
  let triple = total * k                  # escalar: sigue en USD

  let tasa: dec.Decimal = 0.92
  let en_euros: Money[dec.Decimal]<EUR> = money.convert(total, tasa)

  println("total  = #{money.to_string(total)} USD")
  println("triple = #{money.to_string(triple)} USD")
  println("euros  = #{money.to_string(en_euros)} EUR")
}

$ kai run ejemplos/cap19/05_dinero.kai
total  = 15.00 USD
triple = 45.00 USD
euros  = 13.8000 EUR

Sumar la misma moneda, sí. Escalar por un número, sí: el escalado vive en la firma de la operación (Money[t]<c> * t conserva la moneda) y no en el álgebra del kind. Convertir, solo por la puerta explícita de money.convert, con la moneda destino fijada por la anotación. ¿Y multiplicar dos dineros?

# Listado 19.6: ejemplos/cap19/06_usd_por_eur.kai (no compila)
let u: Money[dec.Decimal]<USD> = 10.00<USD>
let e: Money[dec.Decimal]<EUR> = 5.00<EUR>
let sinsentido = u * e          # error: `EUR USD` no existe

$ kai build ejemplos/cap19/06_usd_por_eur.kai
error: operator `*` cannot combine `Currency` quantities: the
result unit `EUR USD` does not exist
  = note: `Currency` habitants stand alone: a quantity is either
    scalar or carries exactly one habitant with exponent 1 —
    habitant products and powers are not expressible

Lee ese error dos veces. Ninguna regla especial para dinero prohíbe la operación: el tipo resultado no se puede formar, porque en el álgebra de Currency no existe un habitante “euros por dólares”. Es la diferencia entre un guardia en la puerta y un edificio sin esa puerta. El mecanismo que le da al físico su kg·m/s^2 le niega al contador su USD*EUR. Basta con dos theories del mismo catálogo.

Así se responde la pregunta que quedó flotando en el capítulo 10: ¿cuándo unit USD y cuándo Money[USD]? Si estás aprendiendo la mecánica de unidades o modelando magnitudes que sí multiplican (precio por energía: USD/kWh por kWh da USD), el kind Measure es tu herramienta. Si estás escribiendo el sistema contable, Currency te quita de encima una familia de tipos sin sentido y te regala Decimal de paso.

19.8 Layout: el orden de los bytes

Cuando serializas un entero a bytes, sea para un protocolo de red, un formato de archivo o un registro binario, tienes que decidir el orden: ¿el byte más significativo primero (big-endian, el orden de red) o al revés (little-endian)? En la mayoría de los lenguajes, elegir mal da un número corrupto que descubres tres capas más abajo. El kind Layout sube esa decisión al tipo.

Un campo de ancho fijo lleva dos cosas: su ancho, que viene del tipo base (U32 mide cuatro bytes, U16 dos), y su orden, que es el habitante. U32<be> y U32<le> son el mismo U32 con representaciones distintas, así que nunca unifican: pasar uno donde se espera el otro no compila. Los dos habitantes, be y le, los trae el stdlib (layout be, layout le) y son un set cerrado; no hay un tercer orden que declarar.

La anotación #[derive(Layout)] sobre un record genera su to_bytes y un shim <tipo>_from_bytes que reconstruye el valor desde un buffer:

# Listado 19.7: ejemplos/cap19/07_layout.kai
#[derive(Layout)]
type Paquete = { magia: U32<be>, puerto: U16<be> }

fn main() : Unit / Stdout {
  let bytes = Paquete { magia: 0<be>, puerto: 0<be> } |> to_bytes()
  match paquete_from_bytes(bytes, 0) {
    Ok(p)  -> println("puerto #{p.value.puerto}")
    Err(m) -> println(m)
  }
}

$ kai run ejemplos/cap19/07_layout.kai
puerto 0

Aquí entra la theory. Composition compone los campos en el orden en que los escribiste, y por eso es asociativa pero no conmutativa: mover un campo cambia el layout. También suma la medida de cada uno, su byte size, para dar el tamaño del record. El over Int del catálogo (kind Layout : Composition over Int) nombra esa medida: un tamaño es un entero y la suma tiene que ser exacta. El resultado es un formato binario posicional y byte-exacto, con el orden verificado en compilación y, como todo kind, borrado del binario.

19.9 Perm: permisos que el tipo persigue

Los kinds que conociste hasta aquí clasifican cantidades: metros, dólares, bytes. Perm clasifica capacidades. Su theory, Semilattice, es la más rara del catálogo, y abre una puerta que los demás kinds no.

El caso concreto vive en la API de archivos del stdlib. Un FileHandle lleva en su tipo lo que el código puede hacer con él. open_read devuelve FileHandle<read>; open_write devuelve FileHandle<read + write>. Y cada operación pide exactamente lo que usa: read_chunk exige <read>, write_chunk exige <write>.

# Listado 19.9: ejemplos/cap19/09_perm.kai
fn primera_linea(h: FileHandle<read>) : String / File =
  match File.read_chunk(h, 64) {
    Ok(s)  -> s
    Err(e) -> e
  }

fn main() : Unit / Stdout + File {
  let ruta = "/tmp/kai_perm_demo.txt"
  match File.open_write(ruta) {
    Ok(h) -> {
      let _ = File.write_chunk(h, "hola, kaikai")
      File.close_file(h)
      match File.open_read(ruta) {
        Ok(r) -> {
          println(primera_linea(r))
          File.close_file(r)
        }
        Err(e) -> println(e)
      }
    }
    Err(e) -> println(e)
  }
}

$ kai run ejemplos/cap19/09_perm.kai
hola, kaikai

Fíjate en primera_linea: pide un FileHandle<read>, pero el handle que abrió open_write es un FileHandle<read + write>, y el programa compila igual. Eso distingue a Semilattice. En los demás kinds, dos habitantes unifican solo si son iguales: U32<be> jamás pasa donde se espera U32<le>. En Perm, unifican por subsunción: un handle con más capacidades sirve donde se piden menos, nunca al revés. read + write incluye read, así que fluye hacia <read>. La dirección importa: un FileHandle<read> puro no compila donde se exige <write>.

fn escribe(h: FileHandle<read>) : Unit / File {
  let _ = File.write_chunk(h, "x")   # no compila: <read> no
  ()                                 # subsume a <write>
}

error: type mismatch in op call File.write_chunk
  --> escribe.kai:2:27
    |
  2 |   let _ = File.write_chunk(h, "x")
    |                           ^
  = note: expected: (FileHandle<write>, String) -> Result[Unit, String]
  = note: found:    (FileHandle<read>, String) -> ?t0

El + de Semilattice es una unión idempotente: read + read es read, el orden no importa (read + write = write + read), y nada se resta. Son las tres leyes que la theory verifica, asociativa, conmutativa e idempotente, y de ahí sale el orden parcial que define la subsunción. Los habitantes read y write los trae la API de archivos (perm read, perm write), y como cualquier kind con palabra introductora, puedes acuñar los tuyos: perm admin, perm audit, lo que tu dominio necesite.

Una precisión honesta: la capacidad es la que tu código declaró al abrir, no el permiso que el sistema operativo tenga en ese instante. Un archivo que desaparece, un chmod a destiempo, siguen apareciendo por el Result de cada operación. Perm te protege de un error de programa, escribir por un handle que abriste para leer. De la realidad del disco no te protege.

19.10 Dim: la forma como índice

Dim es el kind más nuevo y el más distinto de todos. Sus habitantes son valores de Int escritos directamente en <>, sin palabra introductora que los acuñe. <3> es un habitante porque 3 : Int. Y su theory es HindleyMilner, la misma que clasifica los tipos ordinarios: la unificación es la igualdad de primer orden que ya conoces desde el capítulo 3. <3> unifica con <3> y nunca con <4>.

¿Para qué? Para meter la forma de una estructura en su tipo. El caso canónico es Vec[t]<n>: un vector cuyo largo, n, es parte del tipo. Un literal con un largo distinto al que anuncia la anotación no compila.

# Listado 19.10: ejemplos/cap19/10_dim.kai
fn punto[n: Dim](v: Vec[Real]<n>) : Real = v[0]

fn dot[n: Dim](a: Vec[Real]<n>, b: Vec[Real]<n>, i: Int, acc: Real) : Real =
  if i < 0 { acc } else { dot(a, b, i - 1, acc + a[i] * b[i]) }

fn main() : Unit / Stdout {
  let u: Vec[Real]<3> = [1.0, 2.0, 3.0]
  let w: Vec[Real]<3> = [4.0, 5.0, 6.0]
  println("#{punto(u)}")
  println("#{dot(u, w, 2, 0.0)}")
}

$ kai run ejemplos/cap19/10_dim.kai
1
32

punto es genérica sobre el largo: [n: Dim] dice “para cualquier largo”, igual que [u: Measure] decía “para cualquier unidad”. Pero dot va más lejos: sus dos argumentos son Vec[Real]<n> con el mismo n. El tipo obliga a que los vectores midan lo mismo; sumar un <2> con un <3> da un tipo que no se puede formar, en vez de un índice fuera de rango en runtime.

Y el índice equivocado se atrapa donde se escribe:

let a: Vec[Real]<3> = [1.0, 2.0]   # no compila

error: vector literal has 2 elements, but its type fixes the length to 3
  --> largos.kai:4:26
    |
  4 |   let a : Vec[Real]<3> = [1.0, 2.0]
    |                          ^

Como todo kind, Dim se borra en runtime: <3> no ocupa un byte en el binario, es puro andamiaje de compilación. Y como Int es un dominio infinito, Dim es también la demostración de algo que el §19.3 adelantó: una theory puede clasificar más de un kind. HindleyMilner es el motor de Type y de Dim a la vez: igualdad de primer orden sobre dos dominios distintos, tipos en uno, enteros en el otro.

Un límite del álgebra, deliberado: Dim es atómico. Un índice no tiene productos ni potencias: <3*4> y <3^2> no existen. La aritmética a nivel de tipo (concatenar dos vectores para obtener uno de largo n+k) queda fuera de la theory a propósito; sumar esa maquinaria cambiaría el motor de unificación, y Dim prefiere mantenerse en la igualdad simple que hereda de HindleyMilner.

19.11 Shape: el contenedor como habitante

Los kinds con palabra introductora acuñan habitantes de a uno: unit m, currency USD, perm read. Shape no tiene palabra, y esa es su gracia: sus habitantes ya existen. Cada type T[a] de un solo parámetro (List, Vec, Option, tu Caja[a]) es automáticamente un habitante de Shape, su constructor pelado T, igual que cada type es un habitante de Type. No declaras nada nuevo; nombras lo que ya tienes.

Así puedes cuantificar sobre el contenedor además del contenido. Un parámetro [s: Shape] acepta cualquier constructor de un argumento, y s[Int] lo aplica a un tipo:

# Listado 19.8: ejemplos/cap19/08_shape.kai
protocol Contenedor[s: Shape] {
  primero(xs: s[Int]) : Int
}

type Caja[a] = Caja(a)

impl Contenedor for Caja {
  fn primero(xs: Caja[Int]) : Int = match xs {
    Caja(v) -> v
  }
}

impl Contenedor for List {
  fn primero(xs: [Int]) : Int = match xs {
    []         -> 0
    [h, ..._t] -> h
  }
}

fn main() : Unit / Stdout {
  println("caja:  #{primero(Caja(7))}")
  println("lista: #{primero([3, 4, 5])}")
}

$ kai run ejemplos/cap19/08_shape.kai
caja:  7
lista: 3

primero sirve sobre Caja[Int] y sobre [Int] con una sola firma, s[Int] -> Int. La theory ConstructorApp es la que lo permite: al unificar s[Int] con Caja[Int] liga s a Caja, y con [Int] liga s a List; dos shapes unifican solo si son el mismo constructor: List con List, jamás List con Vec. Un shape es atómico, no se compone ni se aplica a medias, así que s[t[Int]] ni siquiera llega a formarse como tipo. Es la expresividad de un functor, abstraer sobre el contenedor, sin los tipos de orden superior que la traen en Haskell: después de monomorfizar, cada llamada es un despacho estático y directo.

19.12 Theory cerrada, modelos abiertos

Cierro con la pregunta de diseño, porque sé que el lector que viene de Haskell la trae cargada: ¿por qué un catálogo cerrado? ¿Por qué no typeclasses, o higher-kinded types, o theories definibles por el usuario, y que cada quien arme su álgebra?

Porque cada entrada del catálogo compra su decidibilidad por separado. La unificación de AbelianGroup es aritmética de exponentes; la de Module, un chequeo de habitante y exponente 1; la de Nominal, igualdad de símbolo. Cada una es un algoritmo pequeño, rápido, sin casos patológicos. Una theory arbitraria definida por el usuario sería un problema de unificación arbitrario, y la historia de los sistemas de tipos está llena de álgebras inocentes con unificación indecidible. El costo caería justo donde kaikai no lo tolera: en el tiempo de compilación y en la calidad de los errores, las dos cosas que este libro lleva dieciocho capítulos defendiendo.

La apuesta de kaikai es theory cerrada, modelos abiertos: el lenguaje trae las álgebras y garantiza que unifican rápido; tú traes los habitantes (unit parsec, currency CLP) y los kinds que esas álgebras admiten (kind Puntos : Module). Es la misma silueta de los protocolos del capítulo 9, single-dispatch cerrado sobre un mecanismo simple en vez de typeclasses abiertas sobre uno complejo, aplicada un piso más arriba.

Lo que el catálogo te da hoy ya lo usaste: dimensiones para el físico, monedas para el contador, arenas para el que persigue microsegundos, y un solo modelo mental para los tres. Y está diseñado para crecer: una entrada nueva es una theory con unificación decidible más una palabra introductora, y el resto del lenguaje (la cuantificación, la sintaxis <...>, el borrado en runtime) la recibe gratis. Qué entradas se ganan el lugar es una conversación de diseño. El mecanismo, como acabas de comprobar, cabe en una pantalla.

Si después de leer el libro te quedas con una sola idea, que sea esta: el lenguaje no es lo que importa; lo que importa es qué te permite construir, y qué te ayuda a evitar construir mal. kaikai apuesta a que con efectos, fibras, contratos, unidades y holes en su lugar, el programador escribe menos código equivocado y más código que merece estar en producción. Si la apuesta funciona para ti, este libro cumplió su propósito.

Gracias por leer hasta aquí. El compilador, el stdlib, los documentos de diseño y los ejemplos viven en github.com/kaikailang-org/kaikai. Hay issues que cerrar y piezas del lenguaje que todavía toman forma. Si este experimento te interesa, hay lugar para que ayudes a mejorarlo.

Ejercicios

19.1. Declara kind Millas : Module with millas y un habitante millas aereas. Escribe una función que sume millas de viajero y otra que las escale por un multiplicador de categoría. Verifica que Int<aereas> * Int<aereas> no compila. ¿Qué dice el error, y en qué se parece al del listado 19.6?

19.2. Toma la cartera multi-moneda del §10.7 y reescríbela con Money[c: Currency] en vez de Real<USD>. ¿Qué cambia en las firmas? ¿Qué error nuevo detecta el compilador que la versión con Measure dejaba pasar?

19.3. En el listado 19.4, cambia sumar(arbol) por arbol como valor del bloque region. Sigue compilando, pero mide con kai bench la versión original contra la nueva construyendo árboles de 10.000 nodos. Explica la diferencia con la letra chica del §19.6.

19.4. El listado 19.3 usa region { ... } sin binder. Extrae la construcción de las dos listas a una función auxiliar fn armar() : ([Int], [Int]) llamada desde dentro del bloque. ¿El programa sigue compilando? ¿Las listas siguen viviendo en la arena? Justifica con la letra chica del §19.6.

19.5. El capítulo 12 mostró que las filas de efectos ignoran el orden: Stdout + Fail unifica con Fail + Stdout. Escribe esa regla como propiedades algebraicas al estilo del catálogo ({ assoc, commut, ... }). ¿Qué propiedad le falta a esa lista para que Fail + Fail colapse a Fail, y qué theory del catálogo ya la declara? ¿Por qué crees que EffectRow es builtin en vez de declararse por propiedades?