隐形眼镜和CPS超过了价值限制

Question

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

相关代码如下：

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)) }

但是每次都必须手动构造这些透镜是乏味的，并且使用诸如CCD_。

有什么办法绕过这里的价值限制吗？

Answer 1

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

在您的情况下，值限制适用于_1值，该值被定义为将镜头函数应用于另外两个函数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_cond，它们分别在具有第一场和第二场的任何记录类型上工作。然后，您可以使用它们来处理不同类型的记录，而不必担心值限制。例如，您可以写：

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 } *)