functional-programming - tipos - inferencias referenciales ejemplos

Crecimiento de la definición de tipo en SML usando la inferencia de tipo de Hindley Milner

Question

Alguien me mostró una vez un pequeño ''truco'' en SML, donde escribió aproximadamente 3 o 4 funciones en su REPL y el tipo resultante para el último valor fue extremadamente largo (como muchos rollos de página largos).

¿Alguien sabe qué código genera un tipo tan largo o si existe un nombre para este tipo de comportamiento?

Answer 1

Los tipos inferidos por la inferencia de tipo Hindley / Milner pueden llegar a ser exponencialmente grandes si los compones 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 anidamiento corresponde al número n de invocaciones de f . En consecuencia, el tipo general tiene tamaño 3 ^ n.

Sin embargo, este no es realmente el peor de los casos, ya que el tipo tiene una estructura regular y se puede representar de manera eficiente mediante un gráfico en el espacio lineal (porque en cada nivel, los tres tipos de constituyentes son iguales y se pueden compartir).

El peor de los casos utiliza la creación de instancias polimórficas para vencer 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 nuevamente es exponencialmente grande, pero a diferencia de lo anterior, todos los tipos de constituyentes son variables de tipo fresco diferentes, 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 de Hindley / Milner es exponencial en el peor de los casos (en espacio y tiempo). Sin embargo, vale la pena señalar que los casos exponenciales solo pueden ocurrir cuando los tipos se vuelven exponencialmente grandes, es decir, en casos, que no se pueden expresar de manera realista sin la inferencia de tipo.