映射多态变体的子集

Question

我经常想要将函数应用于某个变量中的值,以便函数的结果与输入具有相同的类型.如何使类型成功？这是我目前的尝试:

module T : sig
  type generic =
    [ `Foo of int
    | `Bar of int ]

  val map : (int -> int) -> ([< generic] as 'a) -> 'a

(*   val a : [`Foo of int] *)
end = struct
  type generic =
    [ `Foo of int
    | `Bar of int ]

  let map fn = function
    | `Foo x -> `Foo (fn x)
    | `Bar x -> `Bar (fn x)
  let map : (int -> int) -> ([< generic] as 'a) -> 'a = Obj.magic map

(*
  let a : [`Foo of int] = `Foo 1 |> map succ
  let b : [`Bar of int] = `Bar 1 |> map succ
*)
end

这是按原样工作,但如果我取消注释该let a行,那么我得到:

   Values do not match:
     val map : (int -> int) -> [ `Foo of int ] -> [ `Foo of int ]
   is not included in
     val map : (int -> int) -> ([< generic ] as 'a) -> 'a

似乎定义a已经改变了类型map,这似乎很奇怪.

另一方面,在模块结束后放置它:

open T
let a : [`Foo of int] = `Foo 1 |> map succ
let b : [`Bar of int] = `Bar 1 |> map succ

最后,如果我将定义更改map为:

  let map : 'a. (int -> int) -> ([< generic] as 'a) -> 'a = Obj.magic map

(即只是'a.在开头添加一个明确的)然后抱怨:

Error: This definition has type (int -> int) -> ([< generic ] as 'a) -> 'a
   which is less general than
     'b. (int -> int) -> ([< generic ] as 'b) -> 'b

有人可以解释发生了什么吗？有一个更好的方法吗？我可以使用GADT来避免Obj.magic,但是我必须将它传递给每个函数调用,我想避免.

关于真实系统的注意事项

在我实际的程序,我有不同的节点类型(Area,Project,Action,Contact,等)和不同的操作适用于不同的类型,但也有一些普遍的.

例如,with_name可以重命名任何节点类型,但如果我重命名,Action则结果必须是另一个操作.如果我重命名,[Area | Project | Action]那么结果必须是[Area | Project | Action]等等.

我最初使用了一个元组,其中包含常见的细节(例如(name * Action ...)),但是这使得用户很难匹配不同类型(特别是因为它们是抽象的),并且一些特征对于子集是常见的(例如,只有Projects和Actions可以是主演).

Answer 1

您刚刚受到价值限制的影响。类型检查器不知道其中的类型Obj.magic map，特别是它们的单射性/方差，无法立即概括并等待模块边界。如果您使用 merlin 查看，它会向您显示这种类型：(int -> int) -> (_[< generic ] as 'a) -> 'a。请注意，_它显示了单态类型变量。类型变量在第一次使用时会被专门化，因此当您取消注释时会出现这种行为a。

显然，类型检查器设法在模块边界进行泛化，我不会尝试猜测原因，因为涉及（Obj.）魔法。

对此没有明显的好的解决方案，因为 ocaml 不允许您操作行变量，并且在您进入一个分支时不会专门化类型变量，除非使用 gadt （这可能值得一个功能请求。它与此相关））。

如果你的情况很少，或者没有复杂的组合，你可以尝试：

module T : sig
  type foo = FOO
  type bar = BAR

  type _ generic =
    | Foo : int -> foo generic
    | Bar : int -> bar generic

  val map : (int -> int) -> 'a generic -> 'a generic

  val a : foo generic
  val b : bar generic
end = struct

  type foo = FOO
  type bar = BAR

  type _ generic =
    | Foo : int -> foo generic
    | Bar : int -> bar generic

  let map (type a) fn (x : a generic) : a generic = match x with
    | Foo x -> Foo (fn x)
    | Bar x -> Bar (fn x)

  let a = Foo 1 |> map succ
  let b = Bar 1 |> map succ
end