van Laarhoven lens type (as in Haskell)

[infinity0]

Haskell's van Laarhoven lens type has the advantage of performing the getting and setting in one step, avoiding the need to traverse deep complex data structures twice. It looks like this:

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

This can in fact be expressed in ocaml like this:

type ('b, 'a, 't, 's) lens = {
  lens : 'fb 'ft. (('b -> 't) -> 'fb -> 'ft) -> ('a -> 'fb) -> 's -> 'ft
}

The record type is necessary because that is the only place ocaml allows for "internal" polymorphism, and we need an extra initial argument to explicitly supply the fmap function since modular implicits sadly are not yet in OCaml.

But in fact the latter addition can be considered an advantage over Haskell, because we could choose different fmaps for any single data type - e.g. to map either over the first or second element of a pair.

[infinity0]

Upon further exploration, it turns out the above OCaml type is not very easily composable. Haskell picks their definition since those can be composed with normal function composition. However due to the requirement for implicit fmaps it's unlikely we'll get this to work in OCaml, so we might as well do a simpler thing, namely this:

type ('b, 'a, 't, 's) lens = 's -> ('a * ('b -> 't))

This takes a parent value and returns a (child value, setter) pair, where the setter is a closure that is closed over the input parent - thereby giving us the "traverse-only-once" semantics. Then you can define:

let compose
  : type b a t s y x.
    (t, s, y, x) lens ->
    (b, a, t, s) lens ->
    (b, a, y, x) lens = fun lens0 lens1 old_x ->
  let old_s, set0 = lens0 old_x in
  let old_a, set1 = lens1 old_s in
  let set2 b = set0 (set1 b) in
  old_a, set2

let apply lens fmap mknewchild oldparent =
  let oldchild, set = lens oldparent in
  fmap set (mknewchild oldchild)

where apply gives us the Haskell-like usage again.

[pdonadeo]

What do you think @astrada?

Note: Alessandro is the author of Lens.

[astrada]

Nice! Feel free to add them in a new module (to keep both style of lenses).

[pdonadeo]

@infinity0 do you think you can send a pull request?

[infinity0]

Glad you guys like the idea! Sure, I'll start writing up something that can be used.

[infinity0]

I made a start over at https://gist.github.com/infinity0/3c8461ed60d806bb4d6616a03939788a in case anyone has opinions on the final structure. In the meantime I'll keep working on it when I have time.

[infinity0]

Just read through the "Lenses are the coalgebras for the costate comonad" article linked in the README.md. Very interesting. Looks like the s -> (a * (b -> t)) representation I picked above is a "costate comonad", also called a "store comonad".

[llelf]

I made a start over at https://gist.github.com/infinity0/3c8461ed60d806bb4d6616a03939788a

👍 @infinity0 What’s the status of it?

[infinity0]

@llelf Throughout 2017 I developed that code a bit further in a side project I was doing, but never got it to a point where I was satisfied enough with it to release it as a standalone package. There are relationships between the different types of optics that you can't really express in OCaml easily, and it looks like newer theoretical work on lens favours type families based on profunctors rather than the van Laarhoven type families.

I'm not writing OCaml actively these days, but if someone is interested in taking this issue further I can update the gist linked above with the latest version. The main change is the addition of an optic type that lets you compose 2 arbitrary optics - e.g. composing a lens and a prism, or a prism and a traversal, etc. My solution is a bit fudgy however, and I've seen much cleaner solutions in Haskell that are harder to do in OCaml.