为什么我在实现模块类型时不能添加类型约束？

Question

我正在尝试(只是出于兴趣)这样做:

module type CAT = sig
  type ('a, 'b) t
  val id : ('a, 'a) t
  val (@) : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t
end

module Lst = struct
  type ('a, 'b) t = 'a list constraint 'a = 'b
  let id = []
  let (@) = (@)
end

module L : CAT = Lst (* (error) *)

但我得到:

   Type declarations do not match:
     type ('b, 'a) t = 'b list constraint 'a = 'b
   is not included in
     type ('a, 'b) t

为什么这不安全？所有可以看到具体类型的东西也可以看到约束,所以我认为你不能用错误的类型做出某些东西(例如@用(string, int) t参数调用).

---

更新:对于那些说我的模块没有实现签名的人,因为它要求类型相同,请考虑以下(尽管包含List变量中的列表),尽管具有相同的行为:

module Lst = struct
  type ('a, 'b) t =
    List : 'a list  -> ('a, 'a) t

  let id = List []
  let (@) (type a) (type b) (type c) (a:(b, c) t) (b:(a, b) t) : (a, c) t =
    match a, b with
    | List a, List b -> List (a @ b)
end

Answer 1

该示例可以简化为单独的类型定义:

module type S =
sig
  type ('a, 'b) t
end

module M =
struct
  type ('a, 'b) t = 'a list constraint 'a = 'b
end

正如Jeffrey已经指出的那样,M不是类型S,因为它允许更少的应用程序t:根据签名S,类型(int, string) t将是完全合法的(它是格式良好的),但M不允许这种类型((int, string) M.t不是合法类型,因为它违反了明确的约束).

所有这些都完全独立于类型是否实际居住的问题,即是否可以构造类型的值.在您的第二个示例中,模块使相应的类型格式良好,尽管它是无人居住的.无人居住的类型是合法的,有时甚至是有用的(参见例如幻像类型的概念).

Answer 2

类型签名CAT比Lst模块的类型更通用.您还需要将类型约束放在抽象类型上,即type ('a, 'b) t constraint 'a = 'b.

这给了我们以下内容:

module type CAT = sig
  type ('a, 'b) t constraint 'a = 'b
  val id : ('a, 'a) t
  val (@) : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t
end

由toplevel打印如下,在签名中显示单个类型变量(@):

module type CAT = 
  sig
    type ('b, 'a) t constraint 'a = 'b                                          
    val id : ('a, 'a) t
    val ( @ ) : ('c, 'c) t -> ('c, 'c) t -> ('c, 'c) t
  end

"类型x不包括在类型y中"形式的错误消息指的是类型或模块类型作为可能值集的规范,因此使用术语"包括".

在模块实现(Lst)的情况下,我们有一个模块类型.CAT仅当签名与模块的原始签名一样专用(等于设置)或更专用(严格子集)时,才允许将签名(模块类型)应用于模块.

一个人可以写module X : sig val f : unit -> unit end = struct let f x = x end 但不能写module X : sig val f : 'a -> 'a end = struct let f () = () end.后者给出以下错误:

Error: Signature mismatch:
       Modules do not match:
       sig val f : unit -> unit end                                           
       is not included in
         sig val f : 'a -> 'a end
       Values do not match:
         val f : unit -> unit
       is not included in
         val f : 'a -> 'a

这与在某些表达式上放置类型约束不同,在这种情况下,约束是要应用的掩码(与之交叉的集合)而不是子集.例如,let f : unit -> 'a = fun x -> x即使f签名最终unit -> unit成为严格的子集 - 或子类型 - 也可以写unit -> 'a.