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

Question

Je suis en train 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 montre cela, et provoque une erreur de type (ci-dessous), alors que si je supprime simplement les annotations de type, SML il accepte sans problème, ce qui donne toute la fonction 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, un décalage entre les deux clauses de suffixes_helper. Le premier est celui que je ne comprends pas. J'annote d'affirmer que le premier param est de type 'a:list et que le second est du type param 'b:list. Ne doit pas l'algorithme d'inférence de type Hindley-Milner, qui est construit en haut de l'unification générale que 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 types inférées qui interdisant dans un certain sens sont plus strictes que celles données par les annotations de type. Je suppose que cette règle ne serait applicable aux annotations sur les paramètres et une fonction dans son ensemble. Je ne sais pas si cela 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 PMG, mais F #, une autre langue fonctionnelle, donne un avertissement dans ce genre de situation. Donner une erreur peut être un peu dur, mais il est logique: si le programmeur introduit un type supplémentaire variable « b, et si » b doit être de type « une liste, la fonction pourrait ne pas être aussi générique que le programmeur prévu, qui rapporte la valeur.

Answer 2

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

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

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

il est implicitement quantifié 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, ce qui est d'unifier les types. Et vraiment, le système de type de SML est assez simple (pour autant que je sache), il est jamais indécidables, donc des annotations de type explicites ne doivent jamais être nécessaire. Pourquoi voulez-vous les mettre ici?

Answer 3

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