Что вызывает эту ошибку типа Standard-ML?

Question

Я пытался создать хвостовую рекурсивную версию этой очень простой SML-функции:

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

В ходе этого я использовал аннотации типов для параметров.Следующий код показывает это и вызывает ошибку типа (приведенную ниже), тогда как, если я просто удаляю аннотации типа, SML принимает это без проблем, присваивая всей функции ту же подпись, что и более простая функция выше.

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;

Ошибка:

$ 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

Приведены две ошибки.Последнее, по-видимому, здесь менее важно - несоответствие между двумя предложениями suffixes_helper .Первый - это тот, которого я не понимаю.Я комментирую, чтобы указать, что первый параметр имеет тип 'a:list и что второй параметр имеет тип 'b:list.Разве алгоритм вывода типа Хиндли-Милнера, который построен на основе top of general unification, насколько я понимаю, не должен быть способен унифицировать 'b:list с 'a:list list, используя замену 'b ---> 'a list?

Редактировать:Ответ предполагает, что это может иметь какое-то отношение к алгоритму вывода типов, запрещающему выводимые типы, которые в некотором смысле являются более строгими, чем те, которые заданы аннотациями типов.Я бы предположил, что такое правило будет применяться только к аннотациям к параметрам и к функции в целом.Я понятия не имею, правильно ли это.В любом случае, я попытался перенести аннотации типов в тело функции, и я получаю такую же ошибку:

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

Ошибка заключается в том, что сейчас:

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

Я не уверен насчет SML, но F #, другой функциональный язык, выдает предупреждение в подобных ситуациях.Выдача ошибки может быть немного грубой, но это имеет смысл:если программист вводит дополнительную переменную типа 'b, и если 'b должно быть типа 'a list, функция может быть не такой универсальной, как предполагал программист, о чем стоит сообщить.

Answer 2

Это работает:

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 и newacct, 'b list слишком свободно.Когда вы даете явную аннотацию типа

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

это неявно определяется количественно как

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

и очевидно 'b = 'a list не может быть правдой (All a') и (All b') одновременно.

Без явной аннотации типа вывод типа может сделать правильную вещь, которая заключается в унификации типов.И действительно, система типов SML достаточно проста, что (насколько мне известно) она никогда не бывает неразрешимой, поэтому явные аннотации типов никогда не должны быть необходимы.Почему вы хотите поместить их сюда?

Answer 3

Когда вы используете переменные типа, такие как 'a и 'b, это означает , что 'a и 'b может быть установлен на что угодно, независимо.Так, например, это должно сработать, если я решил, что 'b был int и 'a был float;но очевидно, что в данном случае это неверно, потому что получается, что 'b должно быть 'a list.