OCaml递归调用不能有不同的类型参数？

Question

有没有办法进行递归调用但具有不同的类型参数？

这是一个我认为应该编译的例子,但不是.

let swap (a, b) = (b, a)

module Test : sig
  val test : bool option ->
  ('a -> 'b -> 'c) * ('b -> 'a -> 'c)
  -> 'a -> 'b -> 'c
end = struct
  let rec test (b : bool option)
      (f : ('a -> 'b -> 'c) * ('b -> 'a -> 'c))
      (x : 'a) (y : 'b) : 'c =
    match b with
    | None -> (fst f) x y
    | Some true -> (test None f x y)
    | Some false -> (test None (swap f) y x)
end

编译器坚持认为'a和'b在测试中必须是相同的类型,即使没有理由.这是一个错误吗？

Answer 1

这实际上是一个非常有趣的问题.

我之前不知道答案,但通过阅读我面前的两个答案,再加上一些研究,我将尝试解释并在下面回答.

基本上,你想要实现的是这样的签名

val test : bool option -> ('a -> 'b -> 'c) * ('b -> 'a -> 'c) -> 'a -> 'b -> 'c

首先,我要强调的是,试图迫使参数是不同的多态类型,即使用'a, 'b, 'c等,也不会必然迫使OCaml的编译器认为该参数必须有不同的类型.

例如,如果你这样做

let f (x:'a) (y:'b) = x + y;;

看来你强迫x和y成为不同的类型,但是在编译之后,它给出了

val f:int - > int - > int = <fun>

基本上,OCaml无论如何都会这样做type inference,并且如果它不仅仅是针对强制类型,则应用结论.

你可能觉得'a和'b在let f (x:'a) (y:'b) = x + y;;为可能x和y将有不同的类型,也可能是同一类型.所以强制这样的参数类型是没有意义的,对吧？

所以,让我们删除所有强制参数的类型,我们得到

let rec test b f x y =
    match b with
    | None -> (fst f) x y
    | Some true -> test None f x y
    | Some false -> test None (swap f) y x

testOCaml会给出这样的类型:

val测试:bool选项 - >('a - >'a - >'b)*('a - >'a - >'b) - >'a - >'a - >'b = <fun>

所以,基本上,OCaml认为x并且y必须具有相同的类型,并且c不存在因为OCaml的下一个可用类型标签是使用的'b.

为什么x和y必须具有相同的类型？

当OCaml遇到时let rec test b f x y,好吧,它会认为x有类型'a和y类型'b'.

当OCaml的满足| Some true -> test None f x y,没有问题,上述类型推断仍然站立,因为你是通过相同x并y以test一次.

有趣的部分是OCaml遇到的时候| Some false -> test None (swap f) y x.您正在尝试通过y和x(注意订单)test.为了让test工作,x并且y必须具有相同的类型,对不对？

基本上,上面是多态性递归的反面是@Jeffrey Scofield回答的问题.

polymorphism recursion 意味着,函数可以有一些参数,其类型可以在递归期间更改,而不是保持不变.

默认情况下,OCaml当然只允许常量参数类型.

So how does rank 2 polymorphism work?

那怎么解决呢？

你需要一个for_all类型'a..看看我的问题:在OCaml中,这是什么类型的定义:'a.单位 - >'a.

如果我们使用'a.或'a 'b.在类型定义中,则意味着it is really for all types, real polymorphic types, and please, ocaml, do not narrow them down as long as it does not harm.

let rec test : 'a 'b. bool option -> ('a -> 'b -> 'c) * ('b -> 'a -> 'c) -> 'a -> 'b -> 'c =
  fun b f x y ->
    match b with
    | None -> (fst f) x y
    | Some true -> test None f x y
    | Some false -> test None (swap f) y x

以上是测试的新版本.

优力与类型'a 'b.的功能test和'a和'b,ocaml的会觉得他们很都多态,因而参数x和y可以在两个订单被接受.