如何解释SML打字表达式?

要了解这种类型的性质,您需要首先了解 currying .

这样的定义

fun sum a b = a + b

有类型 int -> int -> int .

它是 一 变量(一个整数),其中返回值本身是一个函数,将整数发送到整数。

例如 val f = sum 1 指派 f 将一个添加到其输入的函数(换句话说。, f 5 评估为6。

在实践中,这些函数通常像 sum 3 4 但是那里发生了什么 不是吗 将2个值传递给 sum 相反,传递一个值3,该值返回一个函数,然后将该返回值应用于4。因此, 三加四之和 应解析为 (sum 3) 4 而不是 sum (3,4) --这将是类型错误。

请注意,这与以下内容有根本不同:

fun add (a,b) = a + b

哪一个 是 两个变量的函数,它具有类型 int * int -> int ,这不同于sum的类型 int->int->智力 后者不是前者的语法糖,而是具有根本不同的语义。

当阅读诸如以下内容时: int->int->智力 ,您应该将其视为右关联。换句话说,它与 int -> (int -> int) .

另一件事正在发生 ('a * 'b -> 'b) -> 'b -> 'a list -> 'b 使用 类型变量 'a, 'b 这意味着您试图解析的类型是高阶类型 多态的 'a 和 'b

把它们放在一起, f ,类型 是一个函数,它将任何类型为以下形式的函数作为输入: 'a * 'b -> 'b (返回类型为第二个变量类型的两个变量的函数)。返回值 f 是形式的函数 'b -> 'a list -> 'b 后者是一个函数,它接受类型为的元素 “b 并返回一个函数,该函数发送 'a lists 到类型的对象 “b

你可以这样概括: f 是 咖喱 函数,它接受类型为的函数 ('a * 'b -> 'b) ,类型的值 “b ,类型的值列表 “a ,并返回类型为 “b .这是足够准确的,但不要误认为它等同于类型的函数

('a * 'b -> 'b) * 'b * 'a list -> 'b

顺便说一下,SML中两个最有用的函数, foldl 和 foldr 有类型 ('a*'b->'b)->b->列表->b 因此,这不仅仅是一个学术活动。能够解包此类类型描述是能够正确使用此类函数的关键。

我能够找到一个基于类型推断的解决方案。我以前从未学过这个,但是

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *)

显示函数的参数和返回类型。

(’a * ’b -> ’b) 指第一个参数函数。它需要2个参数( 'b 和 'a )并返回1个值 “b .

“b 引用第二个参数,一个值。

'a list 引用值列表,这是函数中的第三个参数。

最后,最后 “b 是返回值。