¿Qué causa este error de tipo Standard-ML?

Question

Estaba intentando hacer una versión recursiva de cola de esta función SML muy simple:

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

Durante el transcurso de esto, estuve usando anotaciones de tipo en los parámetros.El siguiente código muestra esto y causa un error de tipo (que se muestra a continuación), mientras que si simplemente elimino las anotaciones de tipo, SML lo acepta sin problemas, dándole a toda la función la misma firma que la función más simple anterior.

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;

Error:

$ 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

Se dan dos errores.Esto último parece ser menos importante aquí, una falta de coincidencia entre las dos cláusulas de suffixes_helper.El primero es el que no entiendo.Anoto para indicar que el primer parámetro es de tipo 'a:list y que el segundo parámetro es de tipo 'b:list.¿No debería el algoritmo de inferencia de tipos Hindley-Milner, que está construido sobre la base de la unificación general tal como yo lo entiendo, poder unificar? 'b:list con 'a:list list, utilizando una sustitución de 'b ---> 'a list?

EDITAR:Una respuesta sugiere que puede tener algo que ver con el algoritmo de inferencia de tipos que no permite tipos inferidos que, en cierto sentido, son más estrictos que los dados por las anotaciones de tipo.Supongo que esa regla sólo se aplicaría a las anotaciones sobre parámetros y sobre una función en su conjunto.No tengo idea si esto es correcto.En cualquier caso, intenté mover las anotaciones de tipo al cuerpo de la función y aparece el mismo tipo de error:

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

El error ahora es:

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

No estoy seguro acerca de SML, pero F #, otro lenguaje funcional, da una advertencia en este tipo de situación. Dando un error puede ser un poco duro, pero tiene sentido: si el programador introduce una variable de tipo extra 'b, y si' b debe ser del tipo 'una lista, la función podría no ser tan genérico como el programador pretende, que es digno de mención.

Answer 2

Esto funciona:

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

Como dicen Joh y newacct, 'b list está demasiado flojo.Cuando das la anotación de tipo explícita

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

se cuantifica implícitamente como

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

y obviamente 'b = 'a list No puede ser cierto (All a') y (All b') simultáneamente.

Sin la anotación de tipo explícita, la inferencia de tipos puede hacer lo correcto, que es unificar los tipos.Y realmente, el sistema de tipos de SML es lo suficientemente simple como para que (hasta donde yo sé) nunca sea indecidible, por lo que las anotaciones de tipos explícitas nunca deberían ser necesarias.¿Por qué quieres ponerlos aquí?

Answer 3

Cuando se utiliza como variables de tipo 'a y 'b, lo que significa que 'a y 'b se pueden ajustar a lo , independientemente . Así, por ejemplo, que debería funcionar si decidí que era 'b int y 'a era float; pero obviamente eso no es válido en este caso, porque resulta que 'b debe 'a list.