Quelles sont les causes de cette erreur de type Standard-ML?

Question

je tente de faire une version récursive de cette fonction SML très simple:

fun suffixes [] = [[]] 
    | suffixes (x::xs) = (x::xs) :: suffixes xs; 

Au cours de cela, j'utilisais annotations de type sur les paramaters. Le code suivant le montre et provoque une erreur de type (donnée ci-dessous), alors que si je supprime simplement les annotations de type, SML l'accepte sans problème, donnant à la fonction entière la même signature que la fonction plus simple ci-dessus.

fun suffixes_tail xs = 
    let 
     fun suffixes_helper [] acc = []::acc 
      | suffixes_helper (x::xs:'a list) (acc:'b list) = 
       suffixes_helper xs ((x::xs)::acc) 
    in 
     suffixes_helper xs [] 
    end; 

Erreur:

$ sml typeerror.sml 
Standard ML of New Jersey v110.71 [built: Thu Sep 17 16:48:42 2009] 
[opening typeerror.sml] 
val suffixes = fn : 'a list -> 'a list list 
typeerror.sml:17.81-17.93 Error: operator and operand don't agree [UBOUND match] 
    operator domain: 'a list * 'a list list 
    operand:   'a list * 'b list 
    in expression: 
    (x :: xs) :: acc 
typeerror.sml:16.13-17.94 Error: types of rules don't agree [UBOUND match] 
    earlier rule(s): 'a list * 'Z list list -> 'Z list list 
    this rule: 'a list * 'b list -> 'Y 
    in rule: 
    (x :: xs : 'a list,acc : 'b list) => 
     (suffixes_helper xs) ((x :: xs) :: acc) 
/usr/local/smlnj-110.71/bin/sml: Fatal error -- Uncaught exception Error with 0 
raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27 

Il y a deux erreurs données. Ce dernier semble être moins important ici, une discordance entre les deux clauses de suffixes_helper. Le premier est celui que je ne comprends pas. J'annote pour indiquer que le premier param est de type 'a:list et que le second param est de type 'b:list. Ne devrait pas l'algorithme d'inférence de type Hindley-Milner, qui est construit de haut de l'unification générale si je comprends bien, être en mesure d'unifier 'b:list avec 'a:list list, en utilisant une substitution de 'b ---> 'a list?

EDIT: Une réponse suggère qu'il peut avoir quelque chose à voir avec l'algorithme d'inférence de type interdisant les types inférés qui, dans un certain sens, sont plus stricts que ceux donnés par les annotations de type. Je suppose qu'une telle règle ne s'appliquerait qu'aux annotations sur les paramètres et sur une fonction dans son ensemble. Je n'ai aucune idée si c'est correct. En tout cas, j'ai essayé de déplacer les annotations de type sur le corps de la fonction, et je reçois le même genre d'erreur:

fun suffixes_helper [] acc = []::acc 
    | suffixes_helper (x::xs) acc = 
      suffixes_helper (xs:'a list) (((x::xs)::acc):'b list); 

L'erreur est maintenant:

typeerror.sml:5.67-5.89 Error: expression doesn't match constraint [UBOUND match] 
    expression: 'a list list 
    constraint: 'b list 
    in expression: 
    (x :: xs) :: acc: 'b list 

Answer 1

Je ne suis pas sûr de SML , mais F #, un autre langage fonctionnel, donne un avertissement dans ce genre de situation. Donner une erreur peut être un peu dur, mais cela a du sens: si le programmeur introduit une variable de type supplémentaire 'b, et si' b doit être de type 'une liste, la fonction peut ne pas être aussi générique que prévu par le programmeur, vaut la peine de signaler.

Answer 2

Lorsque vous utilisez des variables de type comme 'a et 'b, cela signifie que 'a et 'b peut être réglé sur quoi que ce soit, indépendamment. Ainsi, par exemple, cela devrait fonctionner si je décidais que 'b était int et 'a était float; mais évidemment ce n'est pas valable dans ce cas car il s'avère que 'b doit être 'a list.

Answer 3

Cela fonctionne:

fun suffixes_tail xs = 
    let 
     fun suffixes_helper [] acc = []::acc 
      | suffixes_helper (x::xs:'a list) (acc:'a list list) = 
       suffixes_helper xs ((x::xs)::acc) 
    in 
     suffixes_helper xs [] 
    end 

Comme Joh et newacct dire 'b list est trop lâche.Lorsque vous donnez l'annotation de type explicite

fun suffixes_helper (_ : 'a list) (_ : 'b list) = ... 

il est implicitement quantifiée comme

fun suffixes_helper (_ : (All 'a).'a list) (_ : (All 'b).'b list) = ... 

et évidemment 'b = 'a list ne peut pas être vrai (All a')et(All b') simultanément.

Sans l'annotation de type explicite, l'inférence de type peut faire la bonne chose, qui est d'unifier les types. Et vraiment, le système de type de SML est assez simple pour que (pour autant que je le sache) il ne soit jamais indécidable, donc les annotations de type explicites ne devraient jamais être nécessaires. Pourquoi voulez-vous les mettre ici?