Quali sono le cause di questo Standard ML tipo di errore?

Question

Stavo cercando di fare un tail-ricorsiva versione di questo molto semplice SML funzione:

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

Durante il corso di questo, io sto usando il tipo di annotazioni sui parametri.Il codice seguente mostra questo e causa un errore di tipo (riportato di seguito), mentre se ho semplicemente rimuovere il tipo di annotazioni, SML accetta senza alcun problema, dando tutta la stessa funzione di una firma come la più semplice funzione di cui sopra.

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;

Errore:

$ 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

Ci sono due errori data.Quest'ultimo sembra essere meno importante, una mancata corrispondenza tra le due clausole di suffixes_helper.Il primo è quello che io non capisco.Ho annotazioni di stato che il primo parametro è di tipo 'a:list e che il secondo parametro è di tipo 'b:list.Non dovrebbe la Hindley-Milner tipo di algoritmo di inferenza, che è costruito in cima generale di unificazione come ho capito, non essere in grado di unificare 'b:list con 'a:list list, utilizzando una sostituzione di 'b ---> 'a list?

EDIT:Una risposta suggerisce che potrebbe avere qualcosa a che fare con il tipo di algoritmo di inferenza per la disattivazione di dedurre i tipi che in un certo senso sono più rigorose rispetto a quelle date dal tipo di annotazioni.Credo che tale regola si applica solo per le annotazioni sui parametri e su una funzione intera.Non ho idea se questo è corretto.In ogni caso, ho provato a spostare il tipo di annotazioni sopra il corpo della funzione, e ho lo stesso tipo di errore:

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

L'errore è ora:

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

Non sono sicuro di SML, ma F #, un altro linguaggio funzionale, dà un avvertimento in questo tipo di situazione. Dare un errore può essere un po 'dura, ma ha senso: se il programmatore introduce un tipo di ulteriore variabile 'b, e se' B deve essere di tipo 'una lista, la funzione potrebbe non essere così generico come il programmatore destinato, che vale la pena di segnalazione.

Answer 2

Questo funziona:

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

Come Joh e newacct dire, 'b list è troppo lento.Quando si dà l'esplicita annotazione di tipo

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

è implicitamente quantificato come

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

e, ovviamente, 'b = 'a list non può essere vero (All a') e (All b') simultaneamente.

Senza l'esplicita annotazione di tipo, tipo di inferenza può fare la cosa giusta, che è quello di unificare i tipi.E davvero, SML tipo di sistema è abbastanza semplice (per quanto ne sono a conoscenza) non è mai di non decidibile, in modo esplicito, le annotazioni di tipo non dovrebbe mai essere necessario.Perché vuoi metterle qui?

Answer 3

Quando si utilizza le variabili di tipo come 'a e 'b, ciò significa che 'a e 'b può essere impostato per niente , in modo indipendente . Così, per esempio dovrebbe funzionare se ho deciso che era 'b int e 'a era float; ma, ovviamente, che non è valido in questo caso perché si scopre che 'b deve essere 'a list.