我注意到有两种方法可以在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
这两种类型对于同一功能有什么区别?还有为什么同一功能有两种类型?
如果我们从你的两个定义中删除语法糖,它们就会成为:
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
x
y
x+y
在第二种情况下, add 是一个函数,它将一个元组作为参数,然后添加元组的两个元素 .
这也解释了两种不同的类型 . -> 是函数箭头,它与右侧相关联,意味着 int -> int -> int 与 int -> (int -> int) 相同,描述了一个带有 int 并返回 int -> int 函数的函数 .
->
int -> int -> int
int -> (int -> int)
int
int -> int
另一方面 * 是用于元组类型的语法,即 int * int 是包含两个整数的元组类型,因此 int * int -> int (括号为 (int * int) -> int ,因为 * 的优先级高于 -> )描述了一个取两元组的函数ints并返回一个int .
*
int * int
int * int -> int
(int * int) -> int
这两个功能不同的原因是由于 Currying 的现象 . 具体来说,Currying是能够使用 dom(f) = R^{n} 编写任何函数作为从 R n -times获取输入的函数 . 这基本上是通过确保每个输入返回下一个要接受的变量的函数来实现的 . 这就是 -> 符号所代表的 - 这是 Curry-Howard Isomorphism 的基本结果 . 所以:
Currying
dom(f) = R^{n}
R
n
Curry-Howard Isomorphism
fun addCurry x y = x + y (* int -> int -> int *) fun addProd (x,y) = x + y (* (int*int) -> int *)
告诉我们 addCurry 是将 addProd 减少为可用于"substitute"并返回变量的形式 . 所以, addProd 和 addCurry 在上下文中是等价的 . 但是,它们在语义上并不等同 . (int*int) 是一种产品类型 . 它说它期望 input1=int 和 input2=int . int -> int 表示需要 int 并返回 int . 这是一个箭头型 .
addCurry
addProd
(int*int)
input1=int
input2=int
如果您有兴趣,您可能还想知道SML函数只有两种参数:
1)咖喱
2)元组 - 所以, fun addProd (x,y) 表示 (x,y) 作为函数参数的元组 .
fun addProd (x,y)
(x,y)
2 回答
如果我们从你的两个定义中删除语法糖,它们就会成为:
和
所以在第一种情况下
add
是一个函数,它接受一个参数x
并返回另一个函数,它接受一个参数y
然后返回x+y
. 这种通过返回另一个函数来模拟多个参数的技术称为currying .在第二种情况下,
add
是一个函数,它将一个元组作为参数,然后添加元组的两个元素 .这也解释了两种不同的类型 .
->
是函数箭头,它与右侧相关联,意味着int -> int -> int
与int -> (int -> int)
相同,描述了一个带有int
并返回int -> int
函数的函数 .另一方面
*
是用于元组类型的语法,即int * int
是包含两个整数的元组类型,因此int * int -> int
(括号为(int * int) -> int
,因为*
的优先级高于->
)描述了一个取两元组的函数ints并返回一个int .这两个功能不同的原因是由于
Currying
的现象 . 具体来说,Currying是能够使用dom(f) = R^{n}
编写任何函数作为从R
n
-times获取输入的函数 . 这基本上是通过确保每个输入返回下一个要接受的变量的函数来实现的 . 这就是->
符号所代表的 - 这是Curry-Howard Isomorphism
的基本结果 . 所以:告诉我们
addCurry
是将addProd
减少为可用于"substitute"并返回变量的形式 . 所以,addProd
和addCurry
在上下文中是等价的 . 但是,它们在语义上并不等同 .(int*int)
是一种产品类型 . 它说它期望input1=int
和input2=int
.int -> int
表示需要int
并返回int
. 这是一个箭头型 .如果您有兴趣,您可能还想知道SML函数只有两种参数:
1)咖喱
2)元组 - 所以,
fun addProd (x,y)
表示(x,y)
作为函数参数的元组 .