高阶函数的类型

Question

如果我为高阶函数指定(我认为)正确的类型,则OCaml编译器拒绝该函数的第二次使用.

代码

let foo ():string  =
    let f: ('a -> string) -> 'a -> string = fun g v -> g v
    in let h = string_of_int
    in let i = string_of_float
    in let x = f h 23
    in let y = f i 23.0
    in x ^ y

导致以下错误消息

File "test.ml", line 6, characters 14-15:
Error: This expression has type float -> string
       but an expression was expected of type int -> string

所以第一次使用f似乎修复了它的第一个参数的类型int -> string.我能理解.但我没有得到的是省略类型限制来f解决问题.

let foo ():string  =
    let f g v = g v
    in let h = string_of_int
    in let i = string_of_float
    in let x = f h 23
    in let y = f i 23.0
    in x ^ y

移动f到全球范围也解决了这个问题:

let f: ('a -> string) -> 'a -> string = fun g v -> g v

let foo ():string  =
  let h = string_of_int
  in let i = string_of_float
  in let x = f h 23
  in let y = f i 23.0
  in x ^ y

为什么第一个例子不能编译而后者的例子呢？

Answer 1

让我用一个更简单的例子说明问题.

# let cons0 (x : 'a) (y : 'a list) = x :: y;;
val cons0 : 'a -> 'a list -> 'a list = <fun>
# let cons1 (x : 'a) (y : 'a list) = x :: y in cons1 1 [];;
- : int list = [1]
# let cons2 (x : 'a) (y : 'a list) = x :: y in (cons2 1 [], cons2 true []);;
This expression has type bool but is here used with type int
# let cons3 x y = x :: y in (cons3 1 [], cons3 true []);;
- : int list * bool list = ([1], [true])

cons0是一个多态函数定义,在全局范围内定义.这对::运营商来说只是一个微不足道的包装.不出所料,该定义有效.cons1几乎相同cons0,除了它的范围仅限于in体内的表达.范围的变化看起来是无害的,而且肯定的是,它的变形.cons3同样的功能,没有类型注释,我们可以在in体内多态地使用它.

那有什么不对cons2？问题在于'a:它是整个顶级短语.定义的短语的语义cons2是

for some type 'a, (let cons2 (x : 'a) (y : 'a list) = ... in ...)

因为'a必须兼容int(由于cons3 1 [])和bool(由于cons3 true [],没有可能的实例化'a.因此该短语是错误的类型.

如果您想根据其通常的类型推断算法考虑ML类型,则每个显式用户变量在统一算法中引入一组约束.这里的约束是'a = "type of the parameter x"和' = "type of the parameter y".但是范围'a是整个短语,它并没有在任何内在范围内推广.因此int,bool两者最终统一到非一般化'a.

最新版本OCaml引入了范围类型变量(如在Niki Yoshiuchi的回答中).在早期版本(≥2.0)中使用本地模块可以实现相同的效果:

let module M = struct
    let cons2 (x : 'a) (y : 'a list) = x :: y
  end in
(M.cons2 1 [], M.cons2 true []);;

(标准MLers注意:这是OCaml和SML不同的地方.)