Polimorfismo Paramétrico de Rango Superior
en Haskell

2012-01-15
(Actualizado el 2012-01-18)

por @joseanpg


El Cálculo Lambda Polimórfico de Girard y Reynolds

Como suele ser frecuente en los tiempos que corren, para entender bien ciertos conceptos lo mejor es ir a las fuentes. En la primera mitad de la decada de los 70 Girard Jean-Yves y John Reynolds formalizaron el Cálculo Lambda Polimórfico, también conocido como Cálculo Lambda de Segundo Orden o System-F.

En su Towards a Theory of Type Structure (1974), Reynolds introduce una extensión del λ-calculus que permite trabajar con variables de tipo como si fueran variables normales. Variables para los tipos de la variables, por este motivo, teniendo en cuenta lo que es el Calculo Lambda básico, creo que el nombre de Cálculo Lambda de Segundo Orden es el más adecuado.

Reynolds comienza introduciendo un "typed lambda calculus" en el que en cada "variable binding" se inserta una expresión en la que se indica a que tipo la variable. Pero lo interesante es que el tipo no se especifica en ese momento, sino que se expresa mediante otra variable que representa al tipo. Veamos el par de ejemplos que Reynolds utiliza en la segunda sección de su artículo (la identidad y la doble aplicación de una función): 

λ x∈t . x

     Donde x es una variable que enlazará un valor 
     del tipo especificado por el valor (tipo) de la variable t

λ f∈t→t . λ x∈t . f (f x)

     Donde f es una variable que enlazará un valor del tipo función con 
       dominio del tipo especificado por el valor de la variable t, 
       codominio del tipo especificado por el valor de la variable t, 

     donde x es una variable que enlazará un valor 
     del tipo especificado por el valor (tipo) de la variable t

Como podéis observar las variables de tipo en las lambdas anteriores son libres. ¿Por qué no tratar a las variables de tipo como a las variables de valor? Demos el paso, introduzcamos una notación para enlazar (binding) las variables de tipo: la lambda mayúscula (Λ). De esta manera Reynolds introduce en su artículo las Funciones Polimorficas.

Veamos como quedan nuestros ejemplos anteriores 

Λ t . λ x∈t . x

Λ t . λ f∈t→t . λ x∈t . f (f x)
Por supuesto podemos β-reducir estas Λ. Por ejemplo: 

  

    
    β-redux
    
  

  

    (Λ t . λ x∈t . x) Integer
    ⇒
    λ x∈Integer . x

En este momento abandono el artículo de Reynolds y paso a construir mis propias explicaciones de lo que nos interesa. Por cierto, a esas reducciones las llamaré Λβ-reducciones.

Notación para el tipo de las funciones polimórficas

Es evidente que vamos a tener que trabajar con funciones polimórficas y funciones básicas que no lo son. Necesitamos una notación que nos permita distinguir el tipo de unas y otras.

El tipo de las funciones entre tipos concretos tiene una notación clara ya conocida. Por ejemplo el tipo de las funciones que tengan dominio A y codominio B, ambos ya especificados, se denota mediante A → B. 

f ≡ λx ∈ A .Expr ∈ B ⇒ f ∈ A → B
Ahora se trata de buscar una notación para las funciones polimórficas. En principio, si una función es una Λ-abstraction que atrapa al tipo de su argumento, el dominio de la función será un tipo cualquiera, es decir, el tipo del dominio puede cuantificarse con el cuantificador universal. Veamos un ejemplo: 
g ≡ Λt.λx∈t.Expr ∈ B

matemáticamente podemos escribir

g ∈ t → B, ∀t ∈ ConjuntoDeTodosLosTipos
Omitamos la referencia explicita al Conjunto de Tipos y coloquemos el cuantificador junto a la variable de tipo: 
g ∈ ∀t . t → B
Esa será la notación que usaremos 
∀t.t → B 

es el tipo de las funciones polimórficas que pueden tener dominio de cualquier tipo
y codominio B

Λt.λx∈t.Expr ∈ B
El resto de casos se dejan como ejercicios para el lector :)

Polimorfísmo de Rango 1

Consideremos de nuevo el segundo ejemplo del artículo de Reynolds, y pongamos un nombre a la función, re 

re ≡ Λ t . λ f∈t→t . λ x∈t . f (f x)
Podemos observar claramente que re es una función polimórfica de tipo: 
re ∈ ∀ t . t → t
Y no lo neguéis, igual de facilmente podemos observar que el argumento de re no es polimórfico: 
f ∈ t → t
Desde el punto de vista del argumento f el tipo t ya está fijado. Observad que nuestra notación funciona bien, no hay cuantificador en este caso.

Diremos que este tipo de funciones polimórficas que pueden tomar como argumento una función no polimórfica tiene Polimorfismo de Rango 1. ¿Adivináis a que llamaremos una función polimórfica de rango 2? Efectivamente a las que toman como argumento otra función polimórfica.

Polimorfísmo de Rango 2

Consideremos el siguiente ejemplo 
-- Polimórfica de tipo ∀t.t→(t,t)

clo ≡ Λt.λx∈t.(x,x) 

-- Polimórfica de tipo ∀a,b,c.(a→c)→(b→c)→a→b→(c,c)

pam ≡ Λa.Λb.Λc.λf∈a→c.λg∈b→c.λx∈a.λy∈b.(f x, g y)

La función pam es polimorfica de rango 1. Supongamos que aplicamos (pam clo clo), es decir vamos a utilizar la misma función polimórfica clo para los dos argumentos funcionales de pam. Como dichos argumentos de pam son no polimórficos (rango 1), el cuerpo de pam utilizará Λβ-reducciones de clo. Para ello habrá que resolver un par de ecuaciones con las variables de tipo, muy fáciles de resolver. 

(pam clo clo) = Λa.Λb.λf∈a→(a,a).λg∈(b,b)→c.λx∈a.λy∈b.(f x, g y)
         where f ≡ λx∈a.(x,x) -- f ∈ a → (a,a) no polimórfica (viene de una Λβ-reducción)
               g ≡ λx∈b.(x,x) -- g ∈ b → (b,b) no polimórfica (viene de una Λβ-reducción)
Claramente hemos intentado utilizar la función polimórfica clo como función a aplicar en el cuerpo de pam pero para ello hemos tenido que pasarla dos veces como argumento.

Estoy seguro de que ya veis venir lo que vamos a hacer: especifiquemos que pam' tome una única función realmente polimórfica como único argumento funcional. Disponemos de notación para ello: 

-- Polimórfica de tipo (∀ t.t->(t,t))->a->b->((a,a),(b,b))


pam' ≡ Λa.Λb.λf∈∀t.t→(t,t).λx∈a.λy∈b.(f x, f y)
Ahora el único argumento funcional f es una función polimórfica. Nuestra función pam' es una Polimórfica de Rango 2.

En Haskell tenemos polimorfismo de rango 1

Vamos a ver que nos dice The Haskell 2010 report respecto al polimorfismo. En el último párrafo de la sección 4.1.3 podéis leer:

With one exception, the type variables in a Haskell type expression are all assumed to be universally quantified; there is no explicit syntax for universal quantification. For example, the type expression a -> a denotes the type ∀ a. a → a.

¿Qué implicaciones tiene lo anterior? Consideremos una simple función polimórfica, de esas que con frecuencia escribimos en Haskell. Por ejemplo nuestra ya conocida clo: 

clo : ∀t . a → (t,t)
clo = Λ t . λ x∈t . (x,x)
En Haskell sería simplemente: 
clo :: t -> (t,t)
clo x = (x,x)
Bien, en realidad en Haskell estamos trabajando con Calculo Lambda de Segundo Orden sujeto a unas cuantas restricciones para que el sistema de inferencia de tipos de Hindley–Milner (HM) funcione sin problemas siempre. Una de las restricciones fundamentales para que el HM funcione con total garantía es que el polimorfismo sea de rango 1.

Rango Superior usando Extensiones de GHC

En GHC disponemos de una extensión que nos permite trabajar con rango superior. El único riesgo que corremos es que tengamos que indicar los tipos de forma explícita en algunos casos. La extensión es: 

{-# LANGUAGE RankNTypes #-}
Si no vamos a pasar de rango 2 también podemos usar 
{-# LANGUAGE Rank2Types #-}

En GHC con la extensión Rank2Types activada, nuestra función pam' sería: 

{-# LANGUAGE Rank2Types #-}

clo :: t -> (t,t) -- el forall.t no es necesario, implícito en Haskell 2010
clo = \ x -> (x,x)

pam' :: (forall t.t->(t,t))->a->b->((a,a),(b,b))
pam' = \ f -> \ x -> \ y -> (f x, f y)
Me gustan las lambdas, por si no os habéis dado cuenta. A continuación os lo muestro de una forma más "ecuacional": 
{-# LANGUAGE Rank2Types #-}

clo :: t -> (t,t) -- el forall.t no es necesario, implícito en Haskell 2010
clo x = (x,x)

pam' :: (forall t.t->(t,t))->a->b->((a,a),(b,b))
pam' f x y = (f x, f y)

Para completar y profundizar