悄悄地将镜头和 CPS 带过价值限制

Question

我正在编写van Laarhoven透镜的一种OCaml编码，但由于值限制而遇到了困难。

相关代码如下：

module Optic : sig
  type (-'s, +'t, +'a, -'b) t
  val lens : ('s -> 'a) -> ('s -> 'b -> 't) -> ('s, 't, 'a, 'b) t
  val _1 : ('a * 'x, 'b * 'x, 'a, 'b) t
end = struct
  type (-'s, +'t, +'a, -'b) t = 
    { op : 'r . ('a -> ('b -> 'r) -> 'r) -> ('s -> ('t -> 'r) -> 'r) }

  let lens get set =
    let op cont this read = cont (get this) (fun b -> read (set this b))
    in { op }

  let _1 = let build (_, b) a = (a, b) in lens fst build
end

我在这里将镜头表示为一种高阶类型，即 CPS 转换函数的转换器 ('a -> 'b) -> ('s -> 't)（正如这里所建议和这里所讨论的）。 函数lens，fst和build都具有完全通用的类型，但它们的组合lens fst build却没有。

Error: Signature mismatch:
       ...
       Values do not match:
         val _1 : ('_a * '_b, '_c * '_b, '_a, '_c) t
       is not included in
         val _1 : ('a * 'x, 'b * 'x, 'a, 'b) t

正如所示的那样，在这个代码片段中，编写_1是完全可行的。

let _1 = { op = fun cont (a, x) read -> cont a (fun b -> read (b, x)) }

但每次手动构建这些镜头都很繁琐，使用高阶函数（如lens）构建它们会更好。

是否有任何方法可以避免这里的值限制？

- J. Abrahamson

---

标准答案是“eta扩展定义”，但在这里你不能这样做，因为那个记录会妨碍。这似乎是一个非常基本的障碍。 - gsg

虽然不太友善，但你仍然可以进行ETA扩展。没有任何东西阻止你将“t”定义为“type (-'s, +'t, +'a, -'b) pre_t = { op : 'r . ('a -> ('b -> 'r) -> 'r) -> ('s -> ('t -> 'r) -> 'r) } type (-'s, +'t, +'a, -'b) t = unit -> ('s, 't, 'a, 'b) pre_t”。 - Pierre Chambart

Answer 1

值限制是OCaml类型系统的一种限制，它防止一些多态值被泛化，即具有普遍量化所有类型变量的类型。这样做是为了在可变引用和副作用存在的情况下保持类型系统的完整性。

在您的情况下，值限制适用于_1值，该值被定义为将lens函数应用于另外两个函数fst和build的结果。lens函数是多态的，但其结果不是，因为它取决于接收到的参数的类型。因此，_1的类型没有完全泛化，不能给它您期望的类型签名。

在这种情况下，有几种可能的方法可以解决值限制问题：

使用显式类型注释来指定要泛化的类型变量。例如，您可以编写：

let _1 : type a b x. (a * x, b * x, a, b) Optic.t = lens fst (fun (_, b) a -> (a, b))

这告诉编译器您希望泛化类型变量a、b和x，并且_1的类型应该是适用于第一和第二组件具有任何类型的对的镜头。

使用函子来抽象类型变量并延迟镜头函数的实例化。例如，您可以编写：

module MakeLens (A : sig type t end) (B : sig type t end) (X : sig type t end) = struct
   let _1 = lens fst (fun (_, b) a -> (a, b))
end

这定义了一个函数对象，它以三个模块作为参数，每个模块都定义了一个类型t，并返回一个包含类型为(A.t * X.t, B.t * X.t, A.t, B.t) Optic.t的值_1的模块。然后，您可以将此函数对象应用于不同的模块，以获得不同的_1实例。例如，您可以编写：

module IntLens = MakeLens (struct type t = int end) (struct type t = int end) (struct type t = string end)
let _1_int = IntLens._1

这将为您提供类型为 (int * string, int * string, int, int) Optic.t 的 _1_int 值。

使用记录代替元组来表示您想要使用镜头操作的数据类型。记录具有命名字段，可以使用点符号访问和更新它们，并且它们比元组更易于多态性。例如，您可以编写：

type ('a, 'x) pair = { first : 'a; second : 'x }
let lens_first = lens (fun p -> p.first) (fun p b -> { p with first = b })
let lens_second = lens (fun p -> p.second) (fun p b -> { p with second = b })

这定义了两个镜头，lens_first 和 lens_second，它们分别作用于任何拥有first和second字段的记录类型上。你可以使用它们来操作不同种类的记录，而无需担心值限制。例如，你可以编写：

type point = { x : int; y : int }
type person = { name : string; age : int }

let p = { x = 1; y = 2 }
let q = lens_first.op (fun x f -> x + 1) p (fun p -> p)
(* q is { x = 2; y = 2 } *)

let r = { name = "Alice"; age = 25 }
let s = lens_second.op (fun x f -> x + 1) r (fun r -> r)
(* s is { name = "Alice"; age = 26 } *)

- PaulvdBoor