如何声明一个模块实现了一个接口，使得签名中的类型与另一种类型相同？

Question

我正在 OCaml 中创建 monad 并且需要组合它们，所以我创建了转换器。我根据带有 Identity monad 的转换器实现了常规 monad：

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

This expression has type 'a option but an expression was expected of type 'b option Identity.m

事实上，编译器除了它的签名是MONAD之外，对Identity一无所知。 (: MONAD) 不仅仅是帮助编译器，它隐藏了关于 Identity 的所有信息，除了它的签名是 MONAD.

因此，您可以为此添加一个类型相等性

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

而且有效。

Answer 2

It seems that now, 'a has replaced 'a m in the signature.

这是破坏性替换的效果，当你写

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

您要求编译器将 'a m 的所有实例替换为 'a。相反，标准 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 = …

如何声明一个模块实现了一个接口，使得签名中的类型与另一种类型相同？

How does one state that a module implements an interface so that a type in the signature is the same as another type?

ocaml

module

functor