O que faz com que esse erro de tipo Standard-ML?

Question

Eu estava tentando fazer uma versão cauda-recursivo desta função SML muito simples:

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

Durante o curso deste, eu estava usando anotações de tipo nas paramaters. O seguinte mostra codificar isso, e faz com que um erro de tipo (dados abaixo), enquanto que se eu simplesmente remover as anotações de tipo, SML aceita-lo sem nenhum problema, dando toda a função a mesma assinatura que a função mais simples acima.

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;

Erro:

$ 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

Há dois erros dadas. Este último parece ser menos importante aqui, uma incompatibilidade entre as duas cláusulas de suffixes_helper. O primeiro é o que eu não entendo. I anotar de estado que o primeiro parâmetro é do tipo 'a:list e que o segundo parâmetro é do tipo 'b:list. Caso não o algoritmo de inferência de tipos Hindley-Milner, que é construído de topo da unificação geral, como eu o entendo, ser capaz de 'b:list unificar com 'a:list list, usando uma substituição de 'b ---> 'a list?

EDIT: Uma resposta sugere que pode ter algo a ver com o algoritmo de inferência de tipos não permitindo tipos inferidos que em certo sentido, são mais rigorosas do que as dadas pelas anotações de tipo. Eu diria que essa regra uma só seria aplicável às anotações sobre os parâmetros e em uma função como um todo. Eu não tenho idéia se isso é correto. Em qualquer caso, eu tentei mover as anotações de tipo para o corpo da função, e eu obter o mesmo tipo de erro:

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

O erro agora é:

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

Eu não estou certo sobre SML, mas F #, outra linguagem funcional, dá um aviso nesse tipo de situação. Dando um erro pode ser um pouco dura, mas faz sentido: se o programador introduz uma variável do tipo extra 'b, e se' b deve ser do tipo 'uma lista, a função pode não ser tão genérico como o programador destina, que vale a pena relatórios.

Answer 2

Isso 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 Joh e digamos newacct, 'b list é muito frouxa. Quando você dá o tipo de anotação explícita

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

é implicitamente quantificado como

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

e, obviamente, 'b = 'a list não pode ser verdade (All a') e (All b') simultaneamente.

Sem o tipo de anotação explícita, a inferência de tipos pode fazer a coisa certa, que é unificar os tipos. E realmente, sistema de tipo de SML é simples o suficiente para que (tanto quanto sei) nunca é indecidível, então anotações de tipo explícitas nunca deveria ser necessário. Por que você quer colocá-los aqui?

Answer 3

Quando você usa variáveis ??do tipo como 'a e 'b, isso significa que 'a e 'b pode ser definido como qualquer , independentemente . Assim, por exemplo, ele deve funcionar se eu decidi que 'b foi int e 'a foi float; mas obviamente que não é válido neste caso, porque acontece que 'b deve ser 'a list.