一个模块如何实现接口，以使签名中的类型与另一种类型相同

Question

我在OCAML中创建单子，需要构成它们，因此我创建了变形金刚。我用身份单元来实施了常规的单调：

module type MONAD = sig
  type 'a m
  val (>>=) : 'a m -> ('a -> 'b m) -> 'b m
  val return : 'a -> 'a m
end
module Identity : MONAD = struct
  type 'a m = 'a
  let (>>=) m f = f m
  let return x = x
end
module OptionT (M : MONAD) : MONAD with type 'a m := ('a option) M.m = struct
  type 'a m = ('a option) M.m
  let (>>=) m f = M.(>>=) m (fun option ->
    match option with
    | Some x -> f x
    | None -> M.return None)
  let return x = M.return @@ Some x
end
module Option = OptionT(Identity)

但是，我不能这样做：

open Option
let _ = (Some 1) >>= (fun x -> Some (x + 1))

错误是：

(Some 1)
This expression has type 'a option
    but an expression was expected of type 'b option Identity.m
Some (x + 1)
This expression has type 'a option
    but an expression was expected of type 'b option Identity.m

如果我尝试使用module Identity : MONAD with type 'a m = 'a解决错误，我会在module Option = OptionT(Identity)上遇到一个错误

The type `m' is required but not provided

现在看来， 'a已在签名中替换 'a m。

做

module Option : MONAD with type 'a m := 'a option = struct
  type 'a m = 'a option
    let (>>=) m f =
      match m with
      | Some x -> f x
      | None -> None
  let return x = Some x
end

工作正常。

我如何告诉编译器模块实现签名，以便在签名中声明的类型与另一种类型相同，同时仍保持签名的原始类型声明？

Answer 1

现在看来，'a替换了'a m在签名中。

当您写

时，这是破坏性替代的效果

module Identity : MONAD with type 'a m := 'a

您要求编译器用'a替换'a m的所有实例。相反，标准with约束在模块类型

中添加了类型平等。

 module Identity : MONAD with type 'a m = 'a

查看您的各种示例，似乎您已经混淆了这两个示例，并且在您打算添加类型约束时使用破坏性替代：

module OptionT(X:Monad) : MONAD with type 'a m = 'a = …
(* or *) module Option : MONAD with type 'a m = 'a option = …

而不是

module OptionT(X:Monad) : MONAD with type 'a m := 'a = …
(* nor *) module Option : MONAD with type 'a m := 'a option = …

Answer 2

此表达式具有'A type'A选项，但期望'B operion Identity的表达式。M

确实，编译器对Identity一无所知，除了其签名是MONAD。(: MONAD(不仅仅是帮助编译器，它隐藏了有关Identity的所有信息，除了其签名是MONAD。

因此，您可以为该

添加类型均等性

module Identity : MONAD with type 'a m = 'a = ...

它有效。