Polimorfismo de rango superior

Abstracción de tipos

Cuando escribimos una abstracción lambda, la idea subyacente es que quién elige el argumento es el llamador y quién elige el retorno es el llamado. En

[$$ (\lambda x:Int.x)3 $$]

el llamador elige que sea 3 el argumento y el llamado elige que sea x(=3) el resultado. Eso sí, el tipo está fijado a

[$$ Int \rightarrow Int $$]

Llamamos "flecha" a la flecha que indica que el tipo es una función de enteros en enteros. Esto es realmente un constructor de tipos.

Cuando usamos un tipo polimórfico el llamador también elige el tipo al que quiere instanciar un término. Para eso usamos una abstracción de tipos (lambda mayúscula). En la versión polimórfica de la función identidad sería:

[$$ (\Lambda T.\lambda x:T.x)Int\ 3 $$]

El llamador debe decidir qué tipo usar (el Int) y qué valor aplicar (el 3). Para expresar que una abstracción requiere un tipo (que puede ser cualquiera), le asignamos un tipo para todo. Así que el tipo de las abstracciones anteriores sería

[$$ \forall X.X \rightarrow X
$$]

Formas canónicas

Es interesante comprobar el hecho inverso. Cuando tenemos un valor cuyo tipo es

[$$ T \rightarrow S $$]

este valor debe ser una abstracción lambda como

[$$ s=\lambda x:T.r $$]

En la anotación del tipo (detrás de la x) tenemos lo que hay a la izquierda de la flecha del tipo. Es decir, el tipo T en la expresión de arriba.

Además, la forma de usarlo es aplicando un valor del propio tipo T. Algo como

[$$ s\ t $$]

donde t tiene tipo T.

Por otra parte, si tenemos un valor cuyo tipo es

[$$ \forall X.T $$]

este valor debe ser una abstracción de tipos como

[$$ s=\Lambda X.t $$]

Y el uso de s sería aplicándole un tipo. Por ejemplo, el tipo R.

[$$ s\ R $$]

Estas son las llamadas formas canónicas y la manera que tenemos de usarlas.

Rango uno

Ahora veamos qué forma puede tener una expresión de tipo

[$$ \forall X. \forall Y. X \rightarrow Y \rightarrow X $$]

Para empezar empieza por un para todo así que debe ser

[$$ \Lambda X.t $$]

Ese término t también empieza por para todo (el de la Y) así que tendríamos

[$$ \Lambda X. \Lambda Y.s $$]

Y el término s una función de dos argumentos que debe tener por tanto dos abstracciones lambda. Para no complicar el término, haremos que el cuerpo final retorne la propia x.

[$$ \Lambda X. \Lambda Y.\lambda x:X. \lambda y:Y. x $$]

Lo interesante de esta expresión es que, al usarla, es el llamador quién elige todos los tipos y argumentos. Podría ser algo como

[$$ (\Lambda X. \Lambda Y.\lambda x:X. \lambda y:Y. x)Int\ String\ 3\ ''hola'' $$]

Siempre que ocurra esto, nuestra expresión será de rango uno. Esto es muy importante porque no hay dependencias de ningún tipo. Dados los argumentos que apliquemos (sean tipos o valores) sabremos, directamente, cómo se van a usar dentro del cuerpo de la función (basta sustituir).

Si modificamos el tipo que hemos usado bajando un para todo a la derecha de una flecha, sólo intercambiamos el orden de los argumentos. Siguen dependiendo todos del llamador.

[$$ \forall X. X \rightarrow \forall Y. (Y \rightarrow X) $$]
[$$ \Lambda X. \lambda x:X. \Lambda Y. \lambda y:Y. x $$]

Seguimos en rango uno.

Rango superior

Ahora vamos a ver qué ocurre cuando ponemos el para todo a la izquierda de una flecha.

[$$ (\forall X.X \rightarrow X)\rightarrow Int $$]

Vemos que lo más exterior es una flecha. Es decir, la forma canónica empezará por lambda minúscula con una anotación de tipo igual a lo que haya a la izquierda de la flecha.

[$$ \lambda x:(\forall X.X \rightarrow X).t $$]

Esto significa que es el llamado el que debe pasarle el tipo a la x dentro de la t. Podría ser algo como

[$$ \lambda x:(\forall X.X \rightarrow X).(x\ Int\ 3) $$]

Entonces, no basta con sustituir, también hemos de calcular con lo que hay dentro del cuerpo de la aplicación. Hemos aumentado en un grado la complejidad con la que tiene que trabajar el sistema de tipos por el mero hecho de escribir un para todo a la izquierda de una flecha.

Si la aparición de este para todo está anidado a la izquierda de las flechas menos de N veces, decimos que el tipo es de rango N. En nuestro caso, como está sólo una vez, es de rango dos.

Es decidible el inferir tipos en rango uno y dos, pero en rango tres y superiores no es decidible. Esa es la razón por la que muchos lenguajes hacen únicamente inferencia de rango dos o, incluso, uno; donde todos los para todos están por fuera de cualquier flecha.