В чем разница между int -> int -> int и (int * int) -> int в SML?

Question

Я заметил, что есть два способа определения функций в SML. Например, если взять функцию надстройки, эти два способа:

fun add x y = x+y; 

fun add(x,y) = x+y; 

Первый метод создает тип функции, как:

val add = fn : int -> int -> int 

Второй создает тип функции как:

val add = fn : int * int -> int 

В чем разница между этими двумя типами для одной и той же функции? А также почему существуют два типа для одной и той же функции?

Answer 1

Если убрать синтаксический сахар из ваших двух определений они становятся:

val add = fn x => fn y => x+y 

и

val add = fn xy => 
    case xy of 
     (x,y) => x+y 

Таким образом, в первом случае add это функция, которая принимает аргумент x и возвращает другую функцию , который принимает аргумент y, а затем возвращает x+y. Этот метод моделирования нескольких аргументов путем возврата другой функции известен как currying.

Во втором случае add - это функция, которая берет кортеж в качестве аргумента, а затем добавляет два элемента кортежа.

Это также объясняет два разных типа. -> - это функция, которая ассоциируется справа, то есть int -> int -> int - это то же самое, что и int -> (int -> int), описывающее функцию, которая принимает int и возвращает функцию int -> int.

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

Answer 2

Причина, по которой эти 2 функции различны, объясняется феноменом Currying. В частности, Currying - это способность записывать любую функцию с dom(f) = R^{n} как функцию, которая принимает входные данные от Rn -times. Это в основном выполняется путем обеспечения того, чтобы каждый вход возвращал функцию для следующей переменной. Это то, что представляет знак ->. Это фундаментальный результат из Curry-Howard Isomorphism. Итак:

fun addCurry x y = x + y (* int -> int -> int *) 
fun addProd (x,y) = x + y (* (int*int) -> int *) 

говорит нам, что addCurry является сокращение addProd в форме, которая может быть использована для «замены» и возвращать переменные. Таким образом, addProd и addCurry являются контекстно-эквивалентными. Однако они не Семантически-эквивалентные. (int*int) - тип продукта. В нем говорится, что он ожидает input1=int и input2=int. int -> int говорит, что он принимает int и возвращает int. Это стрелочный тип.

Если вы заинтересованы, вы можете также хотите знать, что есть только два вида аргументов SML функции:

1) выделанных

2) кортежи - Так, fun addProd (x,y) представляет (x,y) как кортеж к аргументу функции.