在SML中int -> int -> int和( int *int) -> int之间有什么区别？

Question

我注意到在SML中有两种定义函数的方法。例如，如果使用add函数，以下两种方法：

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的元组并返回一个int。

Answer 2

这两种功能之所以不同，是因为存在Currying现象。具体来说，Currying是一种将任何函数写入dom(f) = R^{n}作为从R n-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)表示为函数参数的元组。