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

Question

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

Answer 1

Чтобы понять этот тип sgnature, вам необходимо сначала понять currying.

Определение как

fun sum a b = a + b 

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

Это функция переменная (целое число), где возвращаемое значение само является функцией, которая отправляет ints в 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, которая отличается от типа SUM о 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, так что это не просто академическое упражнение. Возможность распаковывать такие описания типов - это ключ к возможности правильно использовать такие функции.

Answer 2

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

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

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

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

'b ссылается на второй аргумент - значение.

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

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