Понимание ошибки типа: «ожидаемая подпись Int * Int-> Int, но получила Int * Int-> Int»

Question

Комментарии к Стиву Йегге к записи о серверной части Javascript начали обсуждать достоинства систем типов в языках и этот комментарий описывает:

... примеры из систем стиля H-M , где вы можете получить такие вещи, как:

expected signature Int*Int->Int but got Int*Int->Int

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

Кроме того, возможно, я видел подобную ошибку в Miranda ? (Я не использовал его в течение 15 лет, и поэтому моя память об этом смутна)

Answer 1

Я бы взял мнение Йегге (и Олы Бини) о статической типизации с частичкой соли. Если вы понимаете, что дает статическая типизация, вы узнаете, как работает система типов выбранного вами языка программирования.

IIRC, ML использует синтаксис '*' для кортежей. * - это тип кортежа с двумя элементами. Итак, (1, 2) будет иметь тип int * int.

И Haskell, и ML используют -> для функций. В ML int * int -> int будет типом функции, которая принимает кортеж int и int и отображает его в int.

Одна из причин, по которой вы можете увидеть ошибку, которая выглядит смутно, как та, которую Ола цитирует при переходе на ML с другого языка, заключается в том, что вы пытаетесь передать аргументы, используя скобки и запятые, как в C или Pascal, для функция, которая принимает два параметра.

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

Итак, простая функция в ML (примечание: я использую F # в качестве моего ML) может выглядеть примерно так:

let f x y = x + y;;

Имеет тип:

val f : int -> int -> int

(Функция, принимающая целое число и возвращающая функцию, которая сама принимает целое число и возвращает целое число.)

Однако, если вы наивно называете его кортежем:

f(1, 2)

... вы получите ошибку, потому что вы передали int * int чему-то ожидающему int.

Я ожидаю, что это "проблема", в которой Ола пытался бросить оскорбления. Я не думаю, что проблема настолько плоха, как он думает; конечно, в шаблонах C ++ это намного хуже.

Answer 2

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

fun f g = g (1, 2);

f (42, fn x => x * 2)

Это приведет к ошибке типа, подобной следующей:

Ожидаемый тип int * int -> int, полученный тип int * (int -> int)

Если круглые скобки опущены, эта ошибка может быть досадно неоднозначной.

Стоит отметить, что эта проблема далеко не специфическая для Хиндли-Милнера. На самом деле, я не могу вспомнить ни одного странного типа ошибок , характерных для H-M. По крайней мере, ни один из приведенных примеров. Я подозреваю, что Ола просто курил.

Answer 3

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

# let f x = x + 1;;
val f : int -> int = <fun>
# type int = Foo of string;;
type int = Foo of string
# f (Foo "hello");;
This expression has type int but is here used with type int

То, что я здесь сделал, это привязка идентификатора типа int к новому типу, который несовместим со встроенным типом int. Приложив немного больше усилий, мы можем получить более или менее ту же ошибку, что и выше:

# let f g x y = g(x,y) + x + y;;
val f : (int * int -> int) -> int -> int -> int = <fun>
# type int = Foo of int;;
type int = Foo of int
# let h (Foo a, Foo b) = (Foo a);;
val h : int * int -> int = <fun>
# f h;;
This expression has type int * int -> int but is here used with type
  int * int -> int