Crecimiento de la Definición de Tipo en LME Usando la Inferencia de Tipo Hindley Milner

Los tipos que son inferidos por la inferencia de tipo Hindley/Milner pueden llegar a ser exponencialmente grandes si los componemos de la manera correcta. Por ejemplo:

fun f x = (x, x, x)
val t = f (f (f (f (f 0))))

Aquí, t es un triple anidado, cuya profundidad de anidación corresponde al número n de invocaciones de f. En consecuencia, el tipo total tiene tamaño 3^n.

Sin embargo, este no es en realidad el peor caso, ya que el tipo tiene una estructura regular y puede ser representado por un gráfico de manera eficiente en el espacio lineal (porque en cada nivel, los tres tipos constituyentes son los mismos y se pueden compartir).

El peor caso real utiliza la instanciación polimórfica para derrotar esto:

fun f x y z = (x, y, z)
val p1 = (f, f, f)
val p2 = (p1, p1, p1)
val p3 = (p2, p2, p2)

En este caso, el tipo es de nuevo exponencialmente grande, pero a diferencia de lo anterior, todos los tipos constituyentes son diferentes variables de tipo fresco, de modo que incluso una representación gráfica crece exponencialmente (en el número de declaraciones pN).

Así que sí, la inferencia de tipo al estilo Hindley/Milner es exponencial en el peor de los casos (en espacio y tiempo). Vale la pena señalando, sin embargo, que los casos exponenciales solo pueden ocurrir cuando los tipos se vuelven exponencialmente grandes, es decir, en casos, que ni siquiera se puede expresar de manera realista sin inferencia de tipos.