RFC: lenses

[leodemoura]

We have been talking about adding a lenses library similar to the one available in Haskell. Here is a very basic lens in Lean: https://github.com/leanprover/lean/blob/master/tmp/micro_lenses.lean I'm not suggesting we use this basic definition, but I'm using this example to emphasize one issue: performance. I want a "lenses library" that is "destructive update friendly". The current VM performs destructive updates on arrays when their reference counter is one. In the file micro_lenses, we have the following example:

vm_eval let p₀ := (mk_array 10 0, mk_array 5 tt),
            p₁ := (idx 1 ∙ fst)^.set p₀ 1,
            p₂ := (idx 2 ∙ snd)^.set p₁ ff in
        p₂

We have a pair of arrays, and all array updates are performed destructively because: 1- Lenses provide a modify operation which reads and updates a reference. If we had only set and get. We would have to define the lenses.compose set as:

λ a d, s^.set a (t^.set (s^.get a) d)

This definition would prevent destructive updates from being performed in the example above because s would still be alive when we execute t^.set. 2- We define fst and snd using match. The following alternative definition would also prevent destructive updates

def fst {α β} : lens (α × β) α := 
{ modify := λ p f, (f p.1, p.2),
  ... }

since p would still be alive when we execute f.

Ok, we can use lenses to destructively update arrays nested in structures, but the code is not optimal since it reconstructs the pair instead of destructively updating p. This is not a big deal in this case, but suppose we have many layers of nested structures. We use the idiom above in the hash_map library: https://github.com/leanprover/lean/blob/master/library/data/hash_map.lean#L78 We can improve that by making sure the compiler generates better code for structure field lenses. First, they should be automatically generated. Second, the generated code should use a destructive update (when the reference counter is 1) instead of "reconstructing" the structure. With these modification, the hash_map above will be almost as fast as an imperative one when the reference counter is 1.

What else do you want from a lenses library for Lean?

[dselsam]

I'll just list a few simple features I make heavy use of in Haskell. The types are wild, but the basic functionality is simple.

1. Basics

   
   Turn lens into projection:
   view :: FoldLike b a a' b b' -> a -> b

Update inside a structure: over :: ASetter a a' b b' -> (b -> b') -> a -> a'

2. Basics over a MonadState:

Modify field: (%=) :: MonadState a m => Setter a a b b' -> (b -> b') -> m ()

Set field: (.=) :: MonadState a m => Setter a a b b' -> b' -> m ()

Retrieve a field of the state and pass it through the function f: uses :: MonadState a m => Getter a a' b b' -> (b -> r) -> m r

[Kha]

Regarding syntax sugar, we could add a variant of ^. that works on lenses: If l : lens α β, l~.foo could be sugar for β.foo.lens ∙ l (where β.foo.lens is the auto-generated field lens). This can be mixed and matched with user-defined notations:

notation l `~.[` i `]` := idx i ∙ l

... l~.foo~.[2]~.1

You'd still have to name a type explicitly to construct the initial lens. But since we need to know the type of the LHS of ~. anyway, we could also overload it to work on regular values and return "pointed lenses" instead, which in turn would also be accepted by the notation:

structure pointed_lens (α : Type u) (β : Type v) :=
(point : α)
(lens : lens α β)

def compose_lens_pointed_lens {α : Type u} {β : Type v} {σ : Type w} (t : lens β σ) (s : pointed_lens α β) : pointed_lens α σ := ...

infix `∙`:1 := compose_lens_pointed_lens

def pointed_lens.set {α : Type u} {β : Type v} (s : pointed_lens α β) (b : β) : α := ...

infix `~=`:1 := pointed_lens.set

... x~.foo~.[2]~.1 ~= 42

(We could get the behavior of ~. on arbitrary types for free with a coercion from α to pointed_lens α α, but I'm not quite sure whether that is a good idea. Well, I'm not sure whether any of this is a good idea.)

[joehendrix]

In Haskell, I like the ability to compose a lens with a traversal and perform updates using a computation that runs inside a monad as one can with a van Laarhoven-style lens.

If a choice was necessary, I'd rather have the performance of a lens implementation that supports destructive updates, but the easy composition laws on Haskell's lens package are quite nice.

[leodemoura]

In Haskell, I like the ability to compose a lens with a traversal and perform updates using a computation that runs inside a monad as one can with a van Laarhoven-style lens.

@joehendrix I agree, this is very useful.

[leodemoura]

What do we do with dependent records? For example, what would be the fst lens for sigma? We can read/view the first element, but we can't update it (the result would be type incorrect). For dependent records, the updates must be performed simultaneously. These dependencies will be super common. For example, consider the hash_map. https://github.com/leanprover/lean/blob/master/library/data/hash_map.lean#L11-L15

structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
(hash_fn : α → nat)
(size nbuckets : nat)
(nz_buckets : nbuckets > 0)
(buckets : bucket_array α β nbuckets)

when we increase the number of buckets we have to simultaneously increase nbuckets nz_buckets and buckets. I don't see how to do it using lenses.

[gebner]

when we increase the number of buckets we have to simultaneously increase nbuckets nz_buckets and buckets. I don't see how to do it using lenses.

For hash maps, the target of the lens can be a subtype (see full gist):

def nbuckets_lens {α : Type} {β} [decidable_eq α] :
  lens (hash_map α β) {n : ℕ // n > 0} := _

We should probably include proofs of the lens laws in lenses as well.

[leodemoura]

@gebner My point was that most lenses libraries for Haskell generate lenses for structure fields automatically. I don't see how we could generate them in general. Consider the following structure with more constraints.

structure cpoint :=
(x y z : int) (c1 : x < y) (c2 : y < z) (c3 : z < 0)

Users may create lenses for it manually, but the big plus of the lenses libraries is the automatic generation of them.

[gebner]

@leodemoura That's true. As you said, we can still automatically generate getters for them. I have no idea how you would even use a setter for one of the components of cpoint, there is no way you can modify any of the fields independently.

As soon as you have to modify all of the fields together, I don't see any ergonomic advantages of using lenses to access the fields. You can still use the modify combinator to change a cpoint embedded in another structure.

[joehendrix]

I run into this issue regularly when using lenses with GADTs in Haskell, though I don't tend to rely on auto-generated lenses due to the added amount of compilation time from using TemplateHaskell. I'd recommend just generating getters on dependent fields.

When writing functions that modify an existing value, I think the convention should be to make the old value the last argument, e.g., with resizing a hash table, use something like

resize : nat -> hash_map a b -> hash_map a b

This makes it easy to use resize with lens code like using modify.

[cipher1024]

At Galois, we have been using the same formulation of lenses as Kmett. For using lenses in proofs, Kmett nicely identified three laws that they have to obey:

1) You get back what you put in:

view l (set l v s) ≡ v 2) Putting back what you got doesn't change anything:

set l (view l s) s ≡ s 3) Setting twice is the same as setting once:

set l v' (set l v s) ≡ set l v' s

Since by construction, lenses don't obey those laws, I had a hard time writing general theorems about lenses. I came up with the following solution: since Lean nicely blurs the line between types and values, we can use type classes on things that aren't actually types, for instance lenses. So I wrote the following type class:

class lens_laws {s a : Type u} (ln : simple lens s a) :=
  (law1 : ∀ v x, get (@ln (const _) _) (x & ln .~ v) = v)
  (law2 : ∀ x, (x & ln .~ get (@ln (const _) _) x) = x)
  (law3 : ∀ v v' (x : s), ((x & ln .~ v) & ln .~ v') = (x & ln .~ v'))
  (law4 : ∀ x f, (x & ln %~ f) = (x & ln .~ f (get (@ln (const _) _) x)))

I have added law4 to relate "over" to "get" and "set".

I think this solution can be generally applicable. For simple lenses on non-dependent records, instances can be automatically constructed. Consider for example a type 'point', a function for swapping lenses values and a theorem about swapping the coordinates of a point.

First we define the point and its lenses. Proving the lens laws is an additional two lines per lens, not too bad, I think.

import control.lens.lens
import control.lens.axioms

open control.lens

structure point :=
  (x : nat)
  (y : nat)

namespace point

def x_setter (p : point) (x' : nat) := { p with x := x' }
def x_lens : simple lens point nat := @lens.mk _ _ _ _ point.x x_setter

def y_setter (p : point) (y' : nat) := { p with y := y' }
def y_lens : simple lens point nat := @lens.mk _ _ _ _ point.y y_setter

end point

section lens_laws

instance x_lens_well_behaved : lens_laws @point.x_lens :=
by derive_lens_laws

instance y_lens_well_behaved : lens_laws @point.y_lens :=
by derive_lens_laws

end lens_laws

Then we prove a theorem about lenses:

section swap

variables {s a : Type}

def get' (l₀ : simple lens s a) : s → a := get (@l₀ (const _) _)

def swap (l₀ l₁ : simple lens s a) (x : s) : s :=
  x & l₀ .~ get' @l₁ x & l₁ .~ get' @l₀ x

section props

variables l₀ l₁ : simple lens s a
variable x : s
variables [lens_laws @l₁]

theorem swap_left : get' @l₁ (swap @l₀ @l₁ x) = get' @l₀ x := 
begin
  unfold swap get',
  rewrite [lens_get_set] -- this is a nicer name for law1
end

end props

end swap

Notice that one of the extra assumption is that lens l₁ is well-behaved. Since it is encoded as a type class, we don't need to explicitly feed the assumption into the theorem invocation. Using the theorem is then as simple as this:

open point

example (p : point) : get' @y_lens (swap @x_lens @y_lens p) = get' @x_lens p :=
by apply swap_left 

In order to prove swap_right, we would need more information about l₀ and l₁, namely that they are independent. It could be encoded as a type class as well but it will become bulky: for a record with n fields, we need O(n²) instances of independence. Maybe there's a way to make the declaration more concise.

Other downside: those lens laws are of limited use in polymorphic contexts, i.e. when we are interested in a lens of type lens (my_struct a) (my_struct b) a b. I think it is still a nice beginning.

Any thoughts?

[cipher1024]

The nice thing about Kmett's formulation is that a lens can be used either as a getter, a setter or a traversal. In a similar way, using type classes for specification, we can have a hierarchy of type classes so that setter_laws can be inferred from lens_laws and little to no explicit conversion should be needed.

[leodemoura]

@cipher1024 Thanks for sending the feedback, and raising important issues. It is very useful. You are right, we need the lemmas showing field lenses are independent. We can try to avoid the O(n²) overhead by creating these lemmas on demand.

Other downside: those lens laws are of limited use in polymorphic contexts, i.e. when we are interested in a lens of type lens (my_struct a) (my_struct b) a b.

Do you need this kind of lenses?

BTW, in your experience, is the extra pain introduced by lenses when proving properties (e.g. independence lemmas) neutralize the benefits we get from them when writing definitions?

[cipher1024]

Do you need this kind of lenses?

In my current Lean project, I have not needed this extra level of polymorphism. However, I personally really like this kind of lenses in Haskell because they allow a very flexible design idiom where the payload of specialized data structures becomes a type parameter. For example, let's say you're writing some networking code:

constant text : Type
structure network_message {α : Type} : Type := ...

def payload {α β : Type} : lens (network_message α) (network_message β) α β := ...

def await_msg : io (network_message text) := ...

structure user_data : Type := ...

def parse_user_data : text → option user_data := ... 

This kind of design, even without lenses, allows you to write functions on network_message which disregard the type of the payload.

Then you can write a routine to read a user_data from the network with:

def await_user_data : io (network_message user_data) := do
    m ← await_msg,
       -- the expression payload parse_user_data has type 
       -- network_message text → option (network_message user_data)
    match m & payload parse_user_data with
      | (some x) := return x
      | none := fail "malformed user data"
    end

When this kind of design gets nested, it's very handy to have lenses that can change the type of the payload.

BTW, in your experience, is the extra pain introduced by lenses when proving properties (e.g. independence lemmas) neutralize the benefits we get from them when writing definitions?

I have not written too many proofs with lenses yet. So far I have not needed to prove independence at all and the proof of the lens laws have been successfully automated; my data structures are fairly simple. I suspect it might be just as easy to automate the proofs of independence but I have not tried yet. In the simple cases I have seen, the pain is limited to writing out the type of the instances and adding "by derive_XX".

In the most complex cases (e.g. dependency between your fields or doing computation inside the lenses, which I have not encountered in my specifications) it might get more painful but I don't see it offsetting the benefit of using lenses. I'm tempted to see it as the cost of a more complex design. For such designs, it might be reasonable to just not have lenses or to select the lenses carefully.

Is there any plan in Lean to have the tactic language used to generate definitions? This would be a case where it would pay off big time: you could use that feature to generate the lenses themselves, the lens laws and the proofs of independence.

[joehendrix]

Just for some data, I did a quick scan of a moderately large Haskell project we have. It mostly uses manually written lenses. Of the 135 manual lens declarations, 118 (~88%) were simple lenses that where often polymorphic, but did not change the type (e.g., lens (my_struct a) (my_struct a) a a rather than lens (my_struct a) (my_struct b) a b). We also had 8 traversal declarations, and 5 of the eight changed the type (e.g., traversal [a] [b] a b).

I think the common case then would be simple lenses that have enough automation so that there wasn't much added overhead needed to prove theorems about them (like explicit non-aliasing proofs). This automation should ideally also work when composing lenses together (this is used quite a bit).

[jroesch]

@cipher1024 It is already possible to use the tactic language to generate definitions. You can use this API https://github.com/leanprover/lean/blob/master/library/init/meta/tactic.lean#L400.

We even have a couple more involved examples in the standard library, for example this is roughly equivalent to deriving Eq in Haskell (https://github.com/leanprover/lean/blob/master/library/init/meta/mk_dec_eq_instance.lean).

I would love to write a more generic deriving tactical which does the spine of the work and just requires you to fill in each case but I haven't had the time to do it yet.

[cipher1024]

@jroesch Cool! I hadn't seen that. That should help make limit the amount lens-related boiler plate.

The other thing I keep thinking about is how to generalize the lens laws to take full advantage of the flexibility of the four parameters.

What I came up with is:

class gen_lens_laws (F G : Type u → Type u) (ln : Π a b, lens (F a) (F b) (G a) (G b)) :=
  (law1 : ∀ a b (v : G b) (x : F a), 
      get (@ln b b (const _) _) (x & ln a b .~ v) = v)
  (law2 : ∀ a (x : F a), 
      (x & ln a a .~ get (@ln a a (const _) _) x) = x)
  (law3 : ∀ a b c (v : G b) (v' : G c) (x : F a), 
      ((x & ln a b .~ v) & ln b c .~ v') = (x & ln a c .~ v'))
  (law4 : ∀ a b (x : F a) (f : G a → G b), 
      (x & ln a b %~ f) = (x & ln a b .~ f (get (@ln a a (const _) _) x)))

I am not sure if it is maximally general but it is a nice generalization of lens_laws. The type of ln gets a bit awkward though.

It allows the use that I highlighted above: my_lens : Π a b, lens (my_struct a) (my_struct b) a b has an instance of gen_lens_laws my_struct id. Even better, if I wanted my_struct to have a list of 'a' instead of just 'a', this generalization also works:

my_lens : Π a b, lens (my_struct a) (my_struct b) (list a) (list b)
instance : gen_lens_laws my_struct list my_lens

Because of the Π in the type of the lens, I'm unsure how awkward this would be to use. I'll post an update if I come across a use case.

[leodemoura]

We decided that we will not implement this feature in the near future.