隐形眼镜及 CPS 超过价值限制

我正在编码 在 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)) }

但是，每次都必须手工构建这些镜头是非常繁琐的，如果使用高阶函数(如 lens)来构建它们就更好了。

有什么办法可以绕过这个价值限制吗？

2378 次浏览
小开

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

在您的示例中，值限制应用于 _ 1值，该值被定义为将 len 函数应用于另外两个函数 fst 和 build 的结果。Len 函数是多态的，但是它的结果不是，因为它取决于它接收的参数的类型。因此，_ 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 类型，并返回一个包含值 _ 1类型(A.t * X.t，B.t * X.t，A.t，B.t) Optic.t 的模块。然后可以将此函数应用于不同的模块，以获取 _ 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 的 value _ 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 })

这定义了两个透镜，len _ first 和 len _ 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 } *)

提交答案