Haskell — Programación a nivel de tipo

Vectores con longitud indexada

La programación a nivel de tipo implica codificar cierta lógica en el sistema de tipo del lenguaje, que es evaluada y comprobada en tiempo de compilación. Uno de los ejemplos más típicos es el de los vectores con longitud indexada, que añaden la longitud de la lista en el sistema de tipo, evitando estáticamente errores de “fuera de límites”.

Un tipo dependiente es un tipo cuya definición depende del valor. Por ejemplo, un “número entero” es un tipo, mientras que un “número entero impar” es un tipo dependiente, ya que depende del valor del número. A diferencia de otros lenguajes funcionales como Agda, Haskell diferencia entre el nivel de término y el nivel de tipo. Esta distinción hace imposible el uso de tipos dependientes, pero es posible imitar sus efectos mediante el uso de extensiones de GHC.

Números naturales a nivel de tipo

Vamos a codificar nuestros primeros números a nivel de tipo. Para ello, utilizaremos la representación de los números naturales de Peano, donde un número se definen como cero o como el sucesor de un número natural.

Números de Peano

Con esto, acabamos de crear un nuevo tipo de dato llamado Nat, que tiene dos constructores de datos:

  • Zero :: Nat
  • Succ :: Nat -> Nat

y podemos representar los números naturales como:

  • 0 — Zero
  • 1 — Succ Zero
  • 2 — Succ (Succ Zero)
  • 3 — Succ (Succ (Succ Zero))

Es fácil ver que el tipo (:type) de estos datos es Nat. También es fácil ver que el tipo (:kind) del tipo Nat es *. Por lo tanto, lo que tenemos son números naturales a nivel de término. Por ejemplo, podemos implementar una función que dados dos naturales, nos devuelva su suma:

Suma de números de Peano

Pero a nosotros no nos interesa esto. Queremos números naturales a nivel de tipo, no de término, así que tenemos que subir GHC de nivel. La extensión DataKinds nos permite exactamente esto, promover los constructores de datos a constructores de tipos, así como los constructores de tipos a tipos de tipos. Para diferenciarlos, Haskell precede el nombre de estos nuevos constructores con una comilla simple (‘).

Nota. Para utilizar DataKinds en GHCi de forma interactiva, hay que establecer la opción :seti -XDataKinds.

Ahora podemos observar que el tipo (:kind) del tipo ‘Zero es Nat, y el tipo del constructor de tipos ‘Succ es Nat -> Nat; del mismo modo que el tipo del tipo Int es *, y el tipo del constructor de tipos Maybe es * -> *.

Vectores con longitud indexada

Como ya dijimos, los vectores con longitud indexada son listas que añaden su longitud en el sistema de tipo. Para definirlos, necesitamos introducir los tipos de datos algebraicos generalizados (GADTs).

Los GADTs son tipos de datos para los cuales un constructor tiene un tipo no estándar. Esto nos permite proporcionar información adicional del tipo al ajustar los constructores:

Vectores con longitud indexada

Lo primero que observamos es que además de la extensión GADTs hemos añadido la extensión KindSignatures. Esta extensión nos permite anotar el tipo de los tipos en las declaraciones, tal y como anotaríamos el tipo de una expresión. Haskell puede deducirlo perfectamente, así que no es obligatorio, pero así queda explícito que nuestro nuevo constructor de tipos Vector toma un tipo n del tipo Nat (indicando la longitud de la lista) y un tipo a del tipo * (indicando el tipo de dato almacenado en la lista).

Vector tiene dos constructores de datos:

  • VNil, que devuelve un vector de longitud cero.
  • VCons, que toma un dato y un vector de longitud n, y devuelve un vector de longitud n+1. No sabemos qué longitud tiene el vector que recibe, pero sí sabemos que el vector resultante será una unidad más grande.

Operaciones sobre vectores

Genial, ya tenemos nuestros vectores. ¿Y ahora qué? Los hemos creado para trabajar con ellos, así que ahora deberíamos definir algunas operaciones. Por ejemplo, vamos a crear una función que dado un vector nos devuelva su cola. La firma de esta función sería:

tailv :: Vector (‘Succ n) a -> Vector n a

Estamos especificando mediante el tipo, que el resultado de quitar el primer elemento a un vector debe ser un vector con un elemento menos. Tiene sentido. Además, ya de paso estamos descartando los vectores vacíos. Es decir, esta función sólo acepta vectores con longitud mayor que cero. Parece lógico.

Cola de vector con longitud indexada

Si se nos hubiese pasado por la cabeza la — malévola — idea de descartar dos elementos de la lista en lugar de uno, es decir,

tailv (VCons _ (VCons _ xs)) = xs

habríamos obtenido un error de tipo al tratar de compilar el programa. Este tipo de comprobaciones son imposibles con las listas predefinidas de Haskell, ya que no hay información de su longitud en el tipo.

Ahora vamos a crear una función que dados dos vectores de longitud arbitraria n y m, respectivamente, nos devuelva la concatenación de ambos. La firma de esta función sería:

append :: Vector n a -> Vector m a -> Vector (?) a

Mmm… Aquí tenemos un problema, ¿qué ponemos en (?)?. El vector resultante debería tener longitud n+m, pero ¿cómo expresamos esto a nivel de tipo?

A estas operaciones a nivel de tipo se las denomina familias de tipos. Al aplicar una función a los parámetros se produce un tipo. Para utilizarlas, tenemos que incluir la extensión TypeFamilies.

Type families are to vanilla data types what type class methods are to regular functions

Por lo tanto, vamos a crear una familia que dados dos tipos del tipo Nat, nos devuelva un tipo del tipo Nat que represente la suma de ambos. En cierta forma, es similar a la definición de la función add que hemos proporcionado antes a nivel de término.

Suma de números de Peano a nivel de tipo

Ahora sí, podemos crear nuestra función append :: Vector n a -> Vector m a -> Vector (Add n m) a, definida de forma muy similar a la concatenación de dos listas en Haskell:

Concatenación de vectores con longitud indexada

La principal diferencia entre nuestros vectores con longitud indexada y las listas predefinidas en Haskell, es que el sistema de tipo comprobará en tiempo de compilación que la lista resultante de la operación append tiene la longitud correcta. Si en alguna de las ecuaciones de la función no es posible deducir que la longitud es la que debe ser, se producirá un fallo en tiempo de compilación.

¿Dónde está el vector? ¡Que yo lo vea!

A continuación se proporciona el código final completo, junto a una instancia de la clase Show, para los vectores con longitud indexada a nivel de tipo.

Vectores con longitud indexada a nivel de tipo

Podemos observar cómo las funciones tailv y append devuelven el resultado esperado:

  • ghci> tailv (VCons 1 (VCons 2 (VCons 3 VNil)))
    2:3:[]
  • ghci> append (VCons 1 (VCons 2 (VCons 3 VNil))) (VCons 4 VNil)
    1:2:3:4:[]

Ejercicio. Implementa las operaciones más comunes sobre listas para vectores con longitud indexada: map, zipWith, replicate, take y drop.

Ayuda. Puede resultar útil construir las familias de tipos Min (mínimo) y Sub (substracción) para dos números naturales.