OCaml 对象的多态类型问题

Question

在 4.03.0.

我有这段代码，基本上：

module rec First : sig

  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

end = First
and Second : sig

  class foo : object
    method at_least_this_method : First.field
  end

end = Second
and Third : sig

  class usage :
    object

      method action : #Second.foo First.target -> unit

    end

end = struct

  class usage = object
    method action (a : #Second.foo First.target) = ()
  end

end

并且 method action 的最后一行无法键入错误消息：

Error: Some type variables are unbound in this type:
         class usage :
           object method action : #Second.foo First.target -> unit end
       The method action has type (#Second.foo as 'a) First.target -> unit
       where 'a is unbound

我也试过类似的东西：

  class usage = object
    method action = fun (type t) (b : (#Second.foo as t) First.target) -> ()
  end

但那也没有打字。

Answer 1

编辑：请参考下面@gariguejej 的回答以获得更好的解释。

我不是对象类型系统的专家，但这是我的两分钱。

将您的代码更改为：

module rec First : sig

  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

end = First
and Second : sig

  class foo : object
    method at_least_this_method : First.field
  end

end = Second

and Third : sig

  class ['a] usage :
    object
      method action : 'a First.target -> unit
    end

end = struct

  class ['a] usage = object
    method action : 'a First.target -> unit = fun a -> ()
  end

end

使用ocaml -i，我们可以看到'a被约束为constraint 'a = < at_least_this_method : First.field; .. >。

module rec First :
  sig
    type field
    type 'a target = 'a constraint 'a = < at_least_this_method : field; .. >
  end
and Second :
  sig class foo : object method at_least_this_method : First.field end end
and Third :
  sig
    class ['a] usage :
      object
        constraint 'a = < at_least_this_method : First.field; .. >
        method action : 'a First.target -> unit
      end
  end

当然你也可以手动约束'a到<at_least_this_method: field>如果你希望它是一个封闭的对象类型。例如，

module rec First : sig

  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

end = First
and Second : sig

  class foo : object
    method at_least_this_method : First.field
  end

end = Second

and Third : sig

  class ['a] usage :
    object
      constraint 'a = <at_least_this_method:First.field>
      method action : 'a First.target -> unit
    end

end = struct

  class ['a] usage = object
    constraint 'a = <at_least_this_method:First.field>
    method action : 'a First.target -> unit = fun a -> ()
  end

end

参见手册Chapter 3.10

Answer 2

我加一个不成功的试用来解决问题。

#c是一个开放类型，它隐含了一个类型变量来表达..部分对象类型，类型错误是因为这个隐藏类型变量没有被量化。

有趣且令人困惑的是，即使隐藏变量未明确量化，#A.foo 的使用也不会在签名处被拒绝。以下类型检查。（出于对递归模块类型的恐惧，我使用仿函数更改了您的示例）：

module Make(A : sig
  type field
  type 'a target = <at_least_this_method: field; .. > as 'a

  class foo : object
    method at_least_this_method : field
  end
end) = struct
  module type S = sig
    class usage : object
        method action : #A.foo A.target -> unit
    end
  end
  module type S' = sig
    class usage : object
        method action : 'a . (#A.foo as 'a) A.target -> unit
    end
  end

结束

ocamlc -c -i表明签名S和S'的class声明是相同的。 #A.foo内部的类型变量在方法级别进行量化，使action成为多态方法。

@objmagic 的回答是将这种多态性移动到 class 级别。那我们要保持方法多态性怎么办呢？:

class usage = object
  method action : 'a . (#A.foo as 'a) A.target -> unit = assert false
end

但这不进行类型检查：

Error: This expression has type 'a. (#A.foo as 'a) A.target -> unit
       but an expression was expected of type
         'b. (#A.foo as 'b) A.target -> unit
       The type variable 'c occurs inside 'c

类型错误完全是神秘的。对我来说，这是跨越对象类型危险线的标志。每当看到这种报错信息的时候，我天真地认为根本不可能定义这种类型的方法，或者是对象打字的bug，退...

顺便说一句，用那个类型定义一个多态记录是没有问题的：

type t = { action : 'a . (#A.foo as 'a) A.target -> unit }
let t = { action = fun _ -> assert false }

Answer 3

我想你想写下面的代码：

module rec First : sig
  type field
  class type target = object method at_least_this_method: field end
end = First
and Third : sig
  class usage :
    object
      method action : #First.target -> unit
    end
end = struct
  class usage = object
    method action : 'a. (#First.target as 'a) -> unit = fun a -> ()
  end
end

我不确定你为什么在这里使用递归模块。它们不适用于类。特别是，接口不会传播到模块内部的类。这就是为什么您需要在 Third.

的主体中显式编写多态方法 action 的类型

OCaml 对象的多态类型问题

Polymorphism typing problems with OCaml objects

object

polymorphism

ocaml

typing