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

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

0 голосов
/ 06 декабря 2009

Я пытался сделать хвостовую рекурсивную версию этой очень простой функции 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

Даны две ошибки. Последнее кажется здесь менее важным, несоответствие между двумя пунктами суффикса_helper. Первый - тот, который я не понимаю. Я отмечаю, что первый параметр имеет тип 'a:list, а второй - тип 'b:list. Не должен ли алгоритм логического вывода типа Хиндли-Милнера, построенный на вершине общего объединения, насколько я понимаю, быть в состоянии объединить '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

Ответы [ 3 ]

3 голосов
/ 07 декабря 2009

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

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

Как говорят Джо и 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 достаточно проста, чтобы (насколько я знаю) она никогда не была неразрешимой, поэтому явные аннотации типов никогда не должны быть необходимы. Почему вы хотите поместить их здесь?

2 голосов
/ 06 декабря 2009

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

1 голос
/ 06 декабря 2009

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

...