首页 文章

在SML中int - > int - > int和(int * int) - > int有什么区别?

提问于
浏览
1

我注意到有两种方法可以在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

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

2 回答

  • 5

    如果我们从你的两个定义中删除语法糖,它们就会成为:

    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 -> intint -> (int -> int) 相同,描述了一个带有 int 并返回 int -> int 函数的函数 .

    另一方面 * 是用于元组类型的语法,即 int * int 是包含两个整数的元组类型,因此 int * int -> int (括号为 (int * int) -> int ,因为 * 的优先级高于 -> )描述了一个取两元组的函数ints并返回一个int .

  • 0

    这两个功能不同的原因是由于 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 减少为可用于"substitute"并返回变量的形式 . 所以, addProdaddCurry 在上下文中是等价的 . 但是,它们在语义上并不等同 . (int*int) 是一种产品类型 . 它说它期望 input1=intinput2=int . int -> int 表示需要 int 并返回 int . 这是一个箭头型 .

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

    1)咖喱

    2)元组 - 所以, fun addProd (x,y) 表示 (x,y) 作为函数参数的元组 .

相关问题