lean#260 expr lens

Stream: PR reviews

[Gabriel Ebner]

Do we already have something like this? Other opinions?

[Johan Commelin]

Didn't @Keeley Hoek write some sort of expr lens recently for the nth_rewrite tactic?

[Scott Morrison]

It's at https://github.com/leanprover-community/mathlib/blob/master/src/meta/expr_lens.lean

[Scott Morrison]

(I think this is actually a survivor from my work on rewrite_search, even pre-Keeley!)

[Scott Morrison]

I've only looked enough to see that they are not exactly the same, and I sort of doubt it's going to be easy to make something usable in both situations, but I didn't really try to understand @Edward Ayers' version.

[Johan Commelin]

@Scott Morrison Oops, sorry for misattributing

[Edward Ayers]

Hi gang, thanks for the interest!
I added a better set of comments to the PR which I will paste here:

One of the features of the widgets PR is that the lean pretty printer has been modified so that it also tags certain positions in the formatted expression with information about which subexpression of the original expression generated a pariticular part of the pretty printed string. This allows all of the highlighting and lookup of implicit arguments etc in the widget view.

The main thing it introduces is expr.coord which is an enum of labels for each recursive constructor argument in expr. Then an expr.address is simply a list of these coordinates. In this way you can reference subexpressions.

It could also be used to implement lenses (or maybe prisms?) on expressions, that is one could implement

meta def expr.lens {t} [alternative t] : expr.address → (expr → t expr) → (expr → t expr)

which runs the given function on the subexpression and then repackages it.
I didn't include it because I wanted to include in this PR only the minimum amount of stuff that was needed to get to the stage where I had the datatypes and some helper functions for the modified pretty printer.
If people think it doesn't bloat core too much I am happy to include an implementation for the other lensy things.

I also have an implementation of expression zippers in a different project if anyone is interested in that.

[Edward Ayers]

Afaict it's different to Scott's lenses because it includes support for the various binders and also it doesn't include the path construct (I have written a binder-ful version of path elsewhere) for implementing expr zippers. expr.address is just a list of enums that can be used to find a subexpression.

[Edward Ayers]

The other issue is that this file expr_address.lean has to be in init before tactic.show_info is declared.

[Edward Ayers]

So you can't use interactive tactics to derive things

[Scott Morrison]

All sounds good to me. I don't think there's much code-duplication-worry to be concerned about here at this stage, and we are all excited to get widgets asap. :-)

[Patrick Massot]

I vote for widgets asap because I have a propaganda talk scheduled for June 3rd.

[Keeley Hoek]

Indeed, that code is Scott's and I have merely performed an obfuscation pass or two (hence might have seized control of the git blame). Anyway, how is "lens" a name you both came up with!? (or is this common nomenclature? =O)

[Bhavik Mehta]

https://hackage.haskell.org/package/lens :)

[Patrick Massot]

Standard answer when some programming stuff doesn't seem to make any sense at first...

[Kevin Buzzard]

So what I learn from the link is that you can make pong with lenses

[Bhavik Mehta]

https://twitter.com/tangled_zans/status/1208167165104443392

Did you know that trains in the UK run on Lenses? I've been working for @Tracsis for the last five weeks and we're hiring Haskell developers! Please spread the word :)

- Zanzi (@tangled_zans)

[Bhavik Mehta]

If you do want to learn about lenses I recommend: https://skillsmatter.com/skillscasts/4251-lenses-compositional-data-access-and-manipulation

[Patrick Massot]

I've used trains in the UK, and I can totally believe they're ready to try anything to fix them.