【问题标题】:What is the difference between int -> int -> int and (int*int) -> int in SML?SML 中的 int -> int -> int 和 (int*int) -> int 有什么区别?
【发布时间】:2017-02-23 07:29:37
【问题描述】:

我注意到在 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

对于同一个功能,这两种类型有什么区别?还有为什么同一个函数有两种类型?

【问题讨论】:

标签: functional-programming sml smlnj ml


【解决方案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。这种通过返回另一个函数来模拟多个参数的技术称为柯里化。

在第二种情况下,add 是一个函数,它接受一个元组作为参数,然后将元组的两个元素相加。

这也解释了两种不同的类型。 -> 是函数箭头,它与右侧相关联,表示int -> int -> intint -> (int -> int) 相同,描述了一个接受int 并返回int -> int 函数的函数。

另一方面,* 是用于元组类型的语法,即 int * int 是包含两个 int 的元组类型,因此 int * int -> int(括号内为 (int * int) -> int,因为 * 具有更高的优先于->) 描述了一个函数,它接受两个整数的元组并返回一个整数。

【讨论】:

【解决方案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 *)

告诉我们addCurryaddProd 的化简为可用于“替换”和返回变量的形式。所以,addProdaddCurry 是上下文等价的。但是,它们不是语义等价的。 (int*int) 是产品类型。它说它需要input1=intinput2=intint -> int 表示它接受 int 并返回 int。是箭头型的。

如果您有兴趣,您可能还想知道 SML 函数只有 2 种参数:

1) 咖喱

2) 元组 - 因此,fun addProd (x,y)(x,y) 表示为函数参数的元组。

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 2014-10-20
    • 1970-01-01
    • 2020-05-05
    • 2015-11-04
    • 1970-01-01
    • 1970-01-01
    • 2019-08-14
    • 2014-10-19
    相关资源
    最近更新 更多