Sneaking lenses and CPS past the value restriction

I'm encoding a form of van Laarhoven lenses in OCaml, but am having difficulty due to the value restriction.

The relevant code is as follows:

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

Here I am representing a lens as a higher order type, a transformer of CPS-transformed functions ('a -> 'b) -> ('s -> 't) (as was suggested here and discussed here). The functions lens, fst, and build all have fully generalized types but their composition lens fst build does not.

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

As shown in the gist, it's perfectly possible to write _1

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

but having to manually construct these lenses each time is tedious and it would be nice to build them using higher order functions like lens.

Is there any way around the value restriction here?

The value restriction is a limitation of the OCaml type system that prevents some polymorphic values from being generalized, i.e. having a type that is universally quantified over all type variables. This is done to preserve soundness of the type system in the presence of mutable references and side effects.

In your case, the value restriction applies to the _1 value, which is defined as the result of applying the lens function to two other functions, fst and build. The lens function is polymorphic, but its result is not, because it depends on the type of the arguments it receives. Therefore, the type of _1 is not fully generalized, and it cannot be given the type signature you expect.

There are a few possible ways to work around the value restriction in this case:

Use explicit type annotations to specify the type variables you want to generalize. For example, you can write:

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

This tells the compiler that you want to generalize over the type variables a, b, and x, and that the type of _1 should be a lens that works on pairs with any types for the first and second components.

Use functors to abstract over the type variables and delay the instantiation of the lens function. For example, you can write:

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

This defines a functor that takes three modules as arguments, each defining a type t, and returns a module that contains a value _1 of type (A.t * X.t, B.t * X.t, A.t, B.t) Optic.t. You can then apply this functor to different modules to get different instances of _1. For example, you can write:

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

This gives you a value _1_int of type (int * string, int * string, int, int) Optic.t.

Use records instead of tuples to represent the data types you want to manipulate with lenses. Records have named fields, which can be accessed and updated using the dot notation, and they are more amenable to polymorphism than tuples. For example, you can write:

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

This defines two lenses, lens_first and lens_second, that work on any record type that has a first and a second field, respectively. You can then use them to manipulate different kinds of records, without having to worry about the value restriction. For example, you can write:

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

Recommended topics

Hot tags