Как мне интерпретировать это выражение ввода SML?

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *)
fun bar f b nil = b
| bar f b (h::t) = f (h, bar f b t)

Эта функция была дана нам с инструкциями по объяснению того, что она делает. Единственная дополнительная информация заключается в том, что параметры представляют собой двоичную функцию, значение и список. Глядя на него, я уже знаю, что если список равен нулю, он возвращает значение b, в противном случае он применяет двоичную функцию к заголовку списка и рекурсивно. Я просто не понимаю, как интерпретировать эту строку:

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *)

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


typing sml
person tsquared    schedule 06.12.2016    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Чтобы понять эту подпись типа, вам нужно сначала понять каррирование.

Определение, подобное

fun sum a b = a + b

имеет тип int -> int -> int.

Это функция одной переменной (целого числа), где возвращаемое значение само является функцией, которая отправляет целые числа в целые числа.

Например, val f = sum 1 присваивает f функцию, которая добавляет единицу к своему входу (другими словами, функцию-преемник), так что, например, f 5 оценивается как 6.

На практике такие функции часто используются как sum 3 4, но то, что происходит там, не является передачей 2 значений в sum. Вместо этого передается одно значение 3, которое возвращает функцию, и это возвращаемое значение затем применяется к 4. Таким образом, sum 3 4 следует интерпретировать как (sum 3) 4, а не sum (3,4), что было бы ошибкой типа.

Обратите внимание, что это принципиально отличается от чего-то вроде

fun add (a,b) = a + b

которая является функцией двух переменных, имеет тип int * int -> int, который отличается от типа суммы int -> int -> int. Последнее не является синтаксическим сахаром для первого, но имеет принципиально иную семантику.

Читая что-то вроде int -> int -> int, вы должны читать его как правоассоциативное. Другими словами, это то же самое, что и int -> (int -> int).

Еще одна вещь, которая происходит с ('a * 'b -> 'b) -> 'b -> 'a list -> 'b, — это использование переменных типов 'a, 'b. Это означает, что тип, который вы пытаетесь проанализировать, относится к полиморфной функции более высокого порядка. Это 'a и 'b может представлять любой тип.

Собрав все вместе, функция f типа ('a * 'b -> 'b) -> 'b -> 'a list -> 'b — это функция, которая принимает в качестве входных данных любую функцию, тип которой имеет вид 'a * 'b -> 'b (функция двух переменных, возвращаемый тип которой является типом второй переменной). Возвращаемое значение f является функцией вида 'b -> 'a list -> 'b. Последняя представляет собой функцию, которая принимает элемент типа 'b и возвращает функцию, которая отправляет 'a lists объектам типа 'b.

Подводя итог, можно сказать, что f — это каррированная функция, которая принимает функцию типа ('a * 'b -> 'b), значение типа 'b, список значений типа 'a и возвращает значение типа 'b. Это достаточно точно, но не думайте, что это эквивалентно функции типа

('a * 'b -> 'b) * 'b * 'a list -> 'b

Между прочим, две самые полезные функции в SML, foldl и foldr, имеют тип ('a * 'b -> 'b) -> 'b -> 'a list -> 'b, так что это не просто академическое упражнение. Способность распаковывать такие описания типов является ключом к правильному использованию таких функций.

person John Coleman    schedule 06.12.2016

arrow_upward
1
arrow_downward

Мне удалось найти решение, основанное на том, что, по-видимому, называется выводом типов. Я никогда не учился этому раньше, но

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *)

это отображение типов аргументов и возвращаемых значений для функции.

(’a * ’b -> ’b) относится к функции первого аргумента. Он сам требует 2 аргумента ('b и 'a) и возвращает 1 значение 'b.

'b относится ко второму аргументу, значению.

'a list относится к списку значений, третьему аргументу функции.

Наконец, последнее 'b является возвращаемым значением.

person tsquared    schedule 06.12.2016
comment
Функция принимает только один аргумент (который сам по себе является функцией), поэтому использование вами слов «первый», «второй» и т. д. отражает недоразумение. Кроме того, возвращаемое значение является функцией типа ’b -> ’a list -> ’b, а не элементом типа b. Не интерпретируйте каррированную функцию как некаррированную. - person John Coleman; 06.12.2016