Polimorfismo paramétrico

El polimorfismo paramétrico aparece de forma natural en la programación. El caso más simple es la función identidad.

[$$ \lambda x.x $$]

¿Cuál es el tipo de esta función? Realmente, depende de lo que sea el tipo de su argumento. Si es un real, la función será Real->Real. Si es un natural, será Natural->Natural. Si es una cadena Cadena->Cadena.

Esto se puede agrupar con la idea de los tipos universales: Para todo tipo X el resultado es X->X. Lo que se escribe así.

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

Obviamente, según el tipo que deseemos usar, especializamos. Así de 

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

pasamos a

[$$ Real \rightarrow Real $$]

Cuando especializamos X a un real. Pero, ¿podemos especializar X a lo que queramos? ¿Incluso al propio tipo universal? La respuesta es que sí. Es un caso de impredicación en el cual cuantificamos la propia sentencia en la que está el cuantificador. Es decir, que podríamos pasar a especializar

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

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

Y así, infinitamente.

Las estructuras infinitas no son malas de por sí. A menos que quieras recorrerlas enteras. En ese caso vas a tardar un tiempo infinito. Esto es la indecibilidad. Una forma de evitarlo es dividir los tipos en dos. Los esquemas con los para todos y los tipos monomórficos sobre los que se predica.

Esta separación de los tipos en dos niveles es lo que hacen los sistemas de tipos al estilo ML o  de polimorfismo let. Aunque esa será historia para otro post.