0

我仍在试图弄清楚在使用 mirage 时如何拆分代码,它有无数的一流模块。我已经把我需要的一切都放在了一个又大又丑的Context模块中,以避免将十个模块传递给我的所有功能,一个就够痛苦了。

我有一个通过 tcp 接收命令的功能:

let recvCmds (type a) (module Ctx : Context with type chan = a) nodeid chan = ...

经过数小时的反复试验,我发现我需要添加(type a)“显式”type chan = a才能使其工作。看起来很难看,但它可以编译。但是,如果我想让该函数递归:

let rec recvCmds (type a) (module Ctx : Context with type chan = a) nodeid chan =
  Ctx.readMsg chan >>= fun res ->
  ... more stuff ...
  |> OtherModule.getStorageForId (module Ctx)
  ... more stuff ...
  recvCmds (module Ctx) nodeid chan

我通过了两次模块,第一次没问题,但在递归行上出现错误:

The signature for this packaged module couldn't be inferred.

如果我尝试指定我得到的签名

This expression has type a but an expression was expected of type 'a
The type constructor a would escape its scope

似乎我不能使用整个(type chan = a)东西。如果有人可以解释正在发生的事情,以及理想的解决方法,那就太好了。我当然可以使用一段时间,但我宁愿最终理解这些该死的模块。谢谢 !

4

1 回答 1

2

实际的答案是递归函数应该普遍量化它们的局部抽象类型let rec f: type a. .... = fun ...

更准确地说,您的示例可以简化为

module type T = sig type t end 
let rec f (type a) (m: (module T with type t = a)) = f m

产生与您相同的错误:

错误:此表达式具有类型(模块 T 类型为 t = a)但表达式应为 'a 类型 类型构造函数 a 将逃脱其范围

这个错误可以用明确的 forall 量化来修复:这可以用简写符号来完成(对于普遍量化的局部抽象类型):

let rec f: type a.  (module T with type t = a) -> 'never = fun m -> f m

这种行为背后的原因是局部抽象类型不应该逃脱引入它们的函数的范围。例如,这段代码

let ext_store = ref None
let store x = ext_store := Some x
let f (type a) (x:a) = store x

应该明显失败,因为它试图存储 type 的值a,这是f.

因此,具有局部抽象类型的值只能由多态函数使用。例如,这个例子

  let id x = x
  let f (x:a) : a = id x

很好,因为id x适用于任何x.

像这样的功能的问题

 let rec f (type a) (m: (module T with type t = a)) = f m

那么 的类型f在其体内还没有泛化,因为 ML 中的类型泛化发生在let定义处。因此,解决方法是明确告诉编译器f其参数是多态的:

 let rec f: 'a. (module T with type t = 'a) -> 'never =
   fun (type a) (m:(module T with type t = a)) -> f m

这里,'a. ...是一个普遍的量化,应该读作forall 'a. ...。第一行告诉编译器该函数f在其第一个参数中是多态的,而第二行显式地引入了局部抽象类型a以改进打包模块类型。拆分这两个声明非常冗长,因此速记符号结合了两者:

let rec f: type a.  (module T with type t = a) -> 'never = fun m -> f m
于 2018-10-23T19:02:34.247 回答