Ejemplo conciso de costo exponencial de inferencia de tipo ML

Me llamaron la atención que el costo de la inferencia de tipos en un lenguaje funcional como OCaml puede ser muy alto. La afirmación es que hay una secuencia de expresiones tales que para cada expresión la longitud del tipo correspondiente es exponencial en la longitud de la expresión.

Ideé la secuencia a continuación. Mi pregunta es: ¿conoces una secuencia con expresiones más concisas que logre los mismos tipos?

# fun a -> a;;
- : 'a -> 'a = <fun>
# fun b a -> b a;;
- : ('a -> 'b) -> 'a -> 'b = <fun>
# fun c b a -> c b (b a);;
- : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
# fun d c b a -> d c b (c b (b a));;
- : ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
   (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'd
= <fun>
# fun e d c b a -> e d c b (d c b (c b (b a)));;
- : (((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
    (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) ->
   ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
   (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'e
= <fun>
# fun f e d c b a -> f e d c b (e d c b (d c b (c b (b a))));;
- : ((((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
     (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) ->
    ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
    (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'e -> 'f) ->
   (((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
    (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) ->
   ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
   (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'f
= <fun>

En esta respuesta, me atendré a un fragmento central del lenguaje del lenguaje, con solo cálculo lambda y polimórfico letsiguiendo a Hindley-Milner . El lenguaje OCaml completo tiene características adicionales como el polimorfismo de fila (que si no recuerdo mal no cambia la complejidad teórica, pero con el cual los programas reales tienden a tener tipos más grandes) y un sistema de módulos (que si tocas lo suficiente no puede ser -terminativo en casos patológicos que involucran firmas abstractas).

La complejidad de tiempo en el peor de los casos para decidir si un programa ML central tiene un tipo es un simple exponencial en el tamaño del programa. Las referencias clásicas para este resultado son [KTU90] y [M90]. Un tratamiento más elemental pero menos completo se da en [S95].

El tamaño máximo del tipo del tipo de un programa ML central es, de hecho, doblemente exponencial en el tamaño del programa. Si el verificador de tipo debe imprimir el tipo del programa, el tiempo puede ser doblemente exponencial; se puede volver a un simple exponencial definiendo abreviaturas para partes repetidas del árbol. Esto puede corresponder a compartir partes del árbol de tipos en una implementación.

Su ejemplo muestra un crecimiento exponencial del tipo. Sin embargo, tenga en cuenta que es posible dar una representación de tamaño lineal del tipo mediante el uso de abreviaturas para partes repetidas del tipo. Esto puede corresponder a compartir partes del árbol de tipos en una implementación. Por ejemplo:

# fun d c b a -> d c b (c b (b a));;
t2 -> t2
where t2 = (t1 -> 'b -> 'c) -> t1 -> 'a -> 'd
where t1 = 'a -> 'b

(x,x)xpair$N$$\Theta(2^N)$

# let pair x f = f x x;;
# let pairN x = pair (pair (pair … (pair x)…));;
'a -> tN
where tN = (tN-1 -> tN-1 -> 'bN) -> 'bN
…
where t2 = (t1 -> t1 -> 'b2) -> 'b2
where t1 = ('a -> 'a -> 'b1) -> 'b1

Al introducir letdefiniciones polimórficas anidadas , el tamaño del tipo aumenta nuevamente exponencialmente; esta vez, ninguna cantidad de intercambio puede reducir el crecimiento exponencial.

# let pair x f = f x x;;
# let f1 x = pair x in
  let f2 x = f1 (f1 x) in
  let f3 x = f2 (f2 x) in
  fun z -> f3 (fun x -> x) z;;

Referencias

[KTU90] Kfoury, J .; Tiuryn; Urzyczyn, P. (1990). "La capacidad de escritura de ML es completa de deptima". Lecture Notes in Computer Science. CAAP '90 431: 206-220. [ Springer ] [ Google ]

[M90] Mairson, Harry G. (1990). "Decidir la capacidad de escritura ML está completa para el tiempo exponencial determinista". Actas del 17º simposio SIGPLAN-SIGACT de ACM sobre Principios de lenguajes de programación. POPL '90 (ACM): 382–401. [ ACM ]

[P04] Benjamin C. Pierce. Temas avanzados en tipos y lenguajes de programación. MIT Press, 2004. [ Amazon ]

[PR04] François Pottier y Didier Rémy. "La esencia de la inferencia de tipo ML". Capítulo 10 en [P04]. [ pdf ]

[S95] Michael I. Schwartzbach. Inferencia de tipo polimórfico. BRICS LS-95-3, junio de 1995. ps