OCaml将标记函数作为参数/标记函数类型等价

Question

假设函数g定义如下.

utop # let g ~y ~x = x + y ;;
val g : y:int -> x:int -> int = <fun>
utop # g ~x:1 ;;
- : y:int -> int = <fun>
utop # g ~y:2 ;;
- : x:int -> int = <fun>
utop # g ~x:1 ~y:2 ;;
- : int = 3
utop # g ~y:2 ~x:1 ;;
- : int = 3

现在有另一个功能 foo

utop # let foobar (f: x:int -> y:int -> int) = f ~x:1 ~y:2 ;;
val foobar : (x:int -> y:int -> int) -> int = <fun>

可悲的是,当我尝试提供g参数时foobar,它会抱怨:

utop # foobar g ;;
Error: This expression has type y:int -> x:int -> int
       but an expression was expected of type x:int -> y:int -> int

这是非常令人惊讶的,因为我可以成功地进行currify g但不能将其作为参数传递.我用谷歌搜索,发现这篇文章没有多大帮助.我猜这与OCaml的基础类型系统有关(例如标记箭头类型的子类型规则).

那么可以通过OCaml中的任何方式g作为参数传递foobar吗？如果没有,为什么不允许？任何支持文章/书籍/论文就足够了.

Answer 1

关键是标签在运行时不存在.类型X:int -> y:float -> int的函数实际上是一个函数,其第一个参数是int,第二个参数是float.

调用g ~y:123意味着我们将第二个参数123存储在某个地方(在一个闭包中),并且我们将在g最后使用其所有参数调用原始函数时自动使用它.

现在考虑一个更高阶的函数,例如foobar:

let foobar (f : y:float -> x:int -> int) = f ~x:1 ~y:2.

(* which is the same as: *)
let foobar (f : y:float -> x:int -> int) = f 2. 1

f传递给的函数foobar接受两个参数,并且float在运行时必须是第一个参数.

也许有可能支持你的愿望,但这会增加一些开销.为了使以下工作:

let g ~x ~y = x + truncate y;;
foobar g  (* rejected *)

编译器必须创建一个额外的闭包.相反,您需要自己完成,如下所示:

let g ~x ~y = x + truncate y;;
foobar (fun ~y ~x -> g ~x ~y)

通常,OCaml编译器非常简单,不会为您执行这种难以猜测的代码插入.

(我也不是一个理论类型的理论家)