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

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

现在看来,"已经取代了"我的签名.

当你写的时候,这就是破坏性替代的效果

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

你要求编译器替换所有'a mby的实例'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 = …