Exemple concis de coût exponentiel de l'inférence de type ML

11

Il a été porté à mon attention que le coût de l'inférence de type dans un langage fonctionnel comme OCaml peut être très élevé. L'affirmation est qu'il existe une séquence d'expressions telle que pour chaque expression, la longueur du type correspondant est exponentielle sur la longueur de l'expression.

J'ai conçu la séquence ci-dessous. Ma question est: connaissez-vous une séquence avec des expressions plus concises qui réalise les mêmes types?

# 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>
mrrusof
la source

Réponses:

14

Dans cette réponse, je vais m'en tenir à un fragment ML de base du langage, avec juste du lambda-calcul et polymorphe letsuivant Hindley-Milner . Le langage OCaml complet a des fonctionnalités supplémentaires telles que le polymorphisme des lignes (qui si je me souviens bien ne change pas la complexité théorique, mais avec lequel les programmes réels ont tendance à avoir des types plus grands) et un système de modules (qui si vous piquez assez fort peut être non -terminant dans des cas pathologiques impliquant des signatures abstraites).

La complexité temporelle la plus défavorable pour décider si un programme ML de base a un type est une simple exponentielle de la taille du programme. Les références classiques pour ce résultat sont [KTU90] et [M90]. Un traitement plus élémentaire mais moins complet est donné dans [S95].

La taille maximale du type du type d'un programme ML de base est en fait doublement exponentielle dans la taille du programme. Si le vérificateur de type doit imprimer le type du programme, le temps peut donc être doublement exponentiel; il peut être ramené à une exponentielle simple en définissant des abréviations pour des parties répétées de l'arbre. Cela peut correspondre au partage de parties de l'arborescence de types dans une implémentation.

Votre exemple montre une croissance exponentielle du type. Notez, cependant, qu'il est possible de donner une représentation linéaire du type en utilisant des abréviations pour les parties répétées du type. Cela peut correspondre au partage de parties de l'arborescence de types dans une implémentation. Par exemple:

# 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)xpairNΘ(2N)

# 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

En introduisant des letdéfinitions polymorphes imbriquées , la taille du type augmente à nouveau de façon exponentielle; cette fois, aucun partage ne peut raser la croissance exponentielle.

# 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;;

Références

[KTU90] Kfoury, J .; Tiuryn; Urzyczyn, P. (1990). "La typabilité ML est complète dexptime". Notes de cours en informatique. CAAP '90 431: 206-220. [ Springer ] [ Google ]

[M90] Mairson, Harry G. (1990). "Décider la typabilité ML est terminée pour un temps exponentiel déterministe". Actes du 17e symposium ACM SIGPLAN-SIGACT sur les principes des langages de programmation. POPL '90 (ACM): 382–401. [ ACM ]

[P04] Benjamin C. Pierce. Rubriques avancées en types et langages de programmation. MIT Press, 2004. [ Amazon ]

[PR04] François Pottier et Didier Rémy. "L'essence de l'inférence de type ML". Chapitre 10 dans [P04]. [ pdf ]

[S95] Michael I. Schwartzbach. Inférence de type polymorphe. BRICS LS-95-3, juin 1995. ps

Gilles 'SO- arrête d'être méchant'
la source
Donc, fondamentalement, la nature "compositionnelle" des expressions de type couplée à l'inférence de type est la racine du problème?
didierc
1
@didierc Je ne comprends pas votre commentaire. Beaucoup de choses sont compositionnelles. D'une certaine manière, la raison fondamentale est qu'à partir des opérations de base de duplication d'un objet (contrainte que deux types soient identiques) et d'appariement (l' ->opérateur), vous pouvez faire une croissance exponentielle (un arbre de Fibonacci).
Gilles 'SO- arrête d'être méchant'
Oui, je pense que c'est ce que je voulais dire: l'algèbre de type est par définition compositionnelle (vous avez utilisé les termes "composer la fonction de paire" dans votre réponse, c'est probablement là que j'ai choisi le mot), dans le sens où les expressions de type sont construites à partir de des expressions et des opérateurs plus petits, et chaque nouvelle composition d'expressions met à l'échelle la taille de l'expression au moins d'un facteur 2 (avec des types polymorphes plus complexes - triadiques ou plus, le facteur est plus grand).
didierc