参数化本地抽象类型

Question

我试图弄清楚如何编写一个函数取决于具有参数类型的模块,但我无法在任何地方找到类似的东西.我试图尽可能地减少问题,最后得到了这个虚拟的例子.

module type Mappable = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

let plus (type m) (module M : Mappable with type 'a t = 'a m) (xs : int m) = 
  M.map (fun x -> x + 1) xs

这会产生错误Error: Syntax error: module-expr expected.

如果我放弃'a,我最终得到以下错误.

Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match: type t is not included in type 'a t
       They have different arities.

这样做的正确语法是什么？

Answer 1

我相信你想要做的事情在OCaml 4.02.3中是不可能的.让我们看一个没有类型变量的简化版本:

module type Mappable = sig
  type t
  val map : ('a -> 'b) -> t -> t
end

let plus (type m) (module M : Mappable with type t = m) (xs : m) = 
  M.map (fun x -> x + 1) xs

以上是典型的,plus具有以下类型:

val plus : (module Mappable with type t = 'm) -> 'm -> 'm

m其定义中的类型被抽象为变量'm.

现在,回到原始代码并思考该类型plus应具有的内容.既然你正试图抽象m的(type m),它应该是:

val plus : (module Mappable with type 'a t = 'a 'm) -> 'a 'm -> 'a 'm

不幸的是,OCaml不支持允许这种形式的更高级别的多态性'a 'm.似乎第一类模块输入是小心实现的,不是为了介绍它.

您可以看到以下简短的论文,它解释了OCaml中较高kinded多态性的当前(不幸)状态.这解释了一种解决方法:如何在当前的OCaml框架中对其进行编码,并带来显式代价:

https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf

我从未尝试过自己,但同样的解决方法可以应用于您的示例.

Answer 2

在OCaml中不可能,因为类型约束不是常规模块类型约束,而是一种特殊的句法结构,它不允许多态类型:

出现在(模块包类型)类型表达式和带注释的表单中的包类型语法类表示模块类型的子集.该子集由具有可选约束形式约束的命名模块类型组成:只能指定非参数化类型.

通常的解决方法是创建一个模块,将所有类型变量绑定到具体类型:

module type Mapper = sig 
  type a
  type b
  type src
  type dst
  val map : (a -> b) -> src -> dst
end

let plus (type src) (type dst)
    (module M : Mapper with type dst = dst
                        and type src = src
                        and type a = int
                        and type b = int) (xs : src) : dst =
  M.map (fun x -> x + 1) xs

在您的具体的例子,没有必要绑定'a和'b,因为他们本质上不是使用,所以它可以简化为:

module type Mapper = sig 
  type src
  type dst
  val map : ('a -> 'b) -> src -> dst
end

let plus (type src) (type dst)
    (module M : Mapper with type dst = dst
                        and type src = src) (xs : src) : dst =
  M.map (fun x -> x + 1) xs

当然,这是非常有限的,但这是当天可能的.