functional-programming - 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但不能将其作为参数传递。我google了一下，发现this article这没有多大帮助。我猜这与 OCaml 的底层类型系统有关(例如，标记箭头类型的子类型规则)。

那么是否可以通过g作为 foobar 的参数以任何方式在 OCaml 中？如果不是，为什么不允许？任何支持文章/书籍/论文就足够了。

Answer 1

关键是标签在运行时不存在。 X:int -> y:float -> int 类型的函数确实是一个函数，其 第一个 参数是一个整数，其 第二参数是一个浮点数。

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

现在考虑一个高阶函数，例如 foobar :

让 foobar (f : y:float -> x:int -> int) = f ~x:1 ~y:2。

(* 等同于:*)
让 foobar (f : y:float -> x:int -> int) = f 2. 1

函数f传递给 foobar在运行时接受两个参数，并且浮点数必须是第一个参数。

也许可以支持您的愿望，但会增加一些开销。为了使以下工作:

让 g ~x ~y = x + 截断 y;;
foob​​ar g (* 拒绝 *)

编译器必须创建一个额外的闭包。相反，您需要自己做，如下所示:

让 g ~x ~y = x + 截断 y;;
foob​​ar (fun ~y ~x -> g ~x ~y)

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

(我也不是类型理论家)