Lean 4 vs Idris 2

Stream: lean4

[Notification Bot]

Cole Shepherd has marked this topic as unresolved.

[Siddhartha Gadgil]

Having used Idris for a while, a couple of differences I feel:

• The goal of Idris is systems programming, so the book, examples etc are aimed at this. Lean 4 is used for mathematics among other things.
• Lean has many powerful tactics for proving theorems. As I understand Idris is more aimed at "theorems" about correctness of low level software, so these are not a priority (or available).
• A couple of things I like about Idris missing I believe so far in Lean:
  - the hole-filling interface.
  - splitting off a definition
  - breaking a variable being in an inductive type into cases via a keyboard shortcut.

[Mario Carneiro]

I would love to see a short demo, link to a description page, or otherwise extended description of the missing features for people like me who don't have any experience in idris and don't know what they are missing

[Siddhartha Gadgil]

Will look for one (or make one). Some years since I used Idris so these are not at my fingertips.

[Siddhartha Gadgil]

Nice gifs with this are at https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md, specifically the ones I mentioned:

• case split
• attempt to fill a hole
• create top level function

[Mario Carneiro]

your links are pointing to the wrong thing

[Siddhartha Gadgil]

Oops. Will edit

[Siddhartha Gadgil]

Fixed.

I can imagine code-actions to have some of these but it will take work.

[Jireh Loreaux]

Yeah, Idris' feature for creating a top level function felt a lot like extract_lemma, except more polished. I loved that feature in Idris.

[Adam Topaz]

Yeah I would really like to see idris's extract def/lemma for lean.

[Adam Topaz]

There were many situations in LTE, for example, where the proof just gets way too long/slow and where extracting a sublemma was helpful. Itbwould be really great If the editor was able to do that automatically!

[Mario Carneiro]

I have a long list of features I want to implement that are waiting on editor actions that can change the input text, enough that I need to write them down or I'll forget...

[Mario Carneiro]

We need at least Try this:, plus stuff like auto-filling structure instances, just for feature parity with lean 3

[Sebastian Ullrich]

Extracting top-level functions may even be the most tangible goal as it does not require changing existing syntax nor great code formatting

[Mario Carneiro]

Here are some other things I want to try that should be possible once we have editor actions:

• Extract a subterm into a definition
• Change a local variable name (LSP "rename" action)
• Change a global definition name
• Inline variable
• Replace induction' with induction
• Build match/rcases/ intro / rintro application
• tidy self-replacement
• Expand macro in-place
• Replace by tac with the generated term
• Move let / let rec into where clause
• Reformat expression in-place
• Any of the hundreds of editor actions in rust-analyzer, e.g. replace if let with match and back

[Mario Carneiro]

• Auto-insert include line when auto-completing a reference to a declaration which is not imported

[Mario Carneiro]

• build proof skeleton with case bla a b c => done or · done for all the goals at the current point

[David Thrane Christiansen]

• Create an expression to fill a hole that has the right type (results vary based on specificity of type, of course)

[David Thrane Christiansen]

• Generate an entire definition from a type signature

[David Thrane Christiansen]

• Add missing cases to a match expression

[David Thrane Christiansen]

@Mario Carneiro I'd encourage you to spend 4-5 hours and sit down and properly learn Idris or Agda, because there's useful aspects of their user experience that is easier to experience and feel than it is to have explained or see videos about.

[Jason Rute]

@David Thrane Christiansen do you have a recommended tutorial/learning resource for each? (For someone who knows say functional programming and DTT.)

[David Thrane Christiansen]

It's been a few years, so this is likely out of date. But the official Idris tutorial is fine if you already know Haskell or Lean, and easier if you know some dependent types. To get a sense of the feeling of using it, this video is a reasonable place to start - try to do the things he's doing. For Agda, I learned by osmosis from others before the current crop of books, but I've heard good things about PLFA.

[David Thrane Christiansen]

I think their interactive experiences are very similar, and learning one of them is enough to get some of the feeling.

[Siddhartha Gadgil]

The Idris book "Type Driven development with Idris" is very well written (a bit long naturally).

[David Thrane Christiansen]

Yes, that's what I'd recommend to someone who didn't already know dependently-typed programming and wanted to learn Idris.

[David Thrane Christiansen]

But if you just want to get up to speed quickly to get inspiration for good ideas to implement in Lean, then it is perhaps not the most suited.

[Steve Dunham]

I'm currently working through PLFA, and it's been a lot of fun. The first few pages walk through the editor support, so you wouldn't need to go through the whole thing. But the material has been interesting so far. (It looks like Wadler has started to translate it to lean.)

[Jason Rute]

Maybe @Philip Wadler has some thoughts on this topic then.

[Arien Malec]

Any of the hundreds of editor actions in rust-analyzer, e.g. replace if let with match and back

Rust Clippy architecture for Lean 4?

[Kevin Buzzard]

idris.png

[Sky Wilshaw]

More advanced editor support is something I'd be interested in working towards in Lean 4. I have a bit of experience writing LSP programs for my own language, and I hope I could be of use here.

[Philip Wadler]

@Steve Dunham Delighted that you are enjoying PLFA.
@Jason Rute Watch this space for PLFL.

[David Thrane Christiansen]

Kevin Buzzard said:

idris.png

As the author of the Idris Elab monad, I agree that Lean 3's was an improvement over my work, and that Lean 4 is even better. But I think that the snide dismissive attitude that some Lean users express towards other systems, rather than a curious and interested one, is not conducive to the development of the field, nor to the development of Lean.

[Sebastian Ullrich]

At least on my part that seems to have been a weird way of acknowledging prior work. I certainly wouldn't express it that way anymore nowadays, my apologies.

[Sebastian Ullrich]

To be honest I don't even remember anymore what I was referring to. Both systems have some fundamentally different aspects that it's definitely worth studying both of them.

[David Thrane Christiansen]

I just saw it was 2017... In any case, my recollection is that most of the good ideas were in fact independently invented, because neither of us really knew about each other until the fundamentals were already in place, but the Lean 3 design and execution was better than mine was.

[Kevin Buzzard]

Sorry for posting that :-( Yes it was back when the lean chat was about ten people talking privately

[David Thrane Christiansen]

They're certainly shaped by different constraints and approaches - my Idris 1 metaprogramming work was really intended to be used more like Template Haskell is (automated codegen at compile time), rather than like Lean 3's (which was a tactic language). The Lean 4 stuff nicely subsumes both, as well as having some of the nice things from Racket

[David Thrane Christiansen]

Don't worry about it, @Kevin Buzzard :) It stepped on a sore spot for me, which is programming language tribalism. I tend to fall in love with all the languages I use, and want to see them be friends, which makes the normal tendency for people to throw stones at each other into something I perhaps overreact to.

[David Thrane Christiansen]

(you can also find me on the Haskell subreddit recently chastising someone who was asking why Lean isn't just a waste of time given Idris's existence)

[Kevin Buzzard]

When we were talking about Idris in 2017 the lean community was a very different place. I was looking back at old posts for an unrelated reason and ran into it. I am really sorry for posting it.

[David Thrane Christiansen]

It's great to see us all working better together as time marches on

[Kevin Buzzard]

I was very guilty of tribalism in the early stages of Lean 3 and got into some trouble over it. Now my thoughts are almost exactly the opposite -- I would love to see other ITP communities trying to do what we are doing with mathlib but because they are far more dominated by computer scientists I've found it hard to drum up enthusiasm there for research level mathematics. I think "is Lean the best system for mathematics" is an open problem; what we know is that Lean is the most popular system for mathematics, but that's a different claim.

[David Thrane Christiansen]

The thought experiment in Kent Pitman's 1994 essay Lambda: The Ultimate Political Party suggests that by being popular for mathematics, Lean will become the best for it. His point is that programming languages (and by extension ITPs) will, over time, adapt to the values of their user communities. As he puts it:

Languages are a reflection of the community they serve. They become the way we express process, and so they inform our sense of what processes we expect.

But time will tell!

[Wojciech Nawrocki]

Mario Carneiro said:

I have a long list of features I want to implement that are waiting on editor actions that can change the input text, enough that I need to write them down or I'll forget...

To come back to this, what do you mean by "editor actions that can change the input text"? We can already register custom code actions that edit the file. The only substantial missing piece is syntax-aware edits; currently it is just strings so it's easy to emit something that doesn't parse. But it's no worse than Lean 3's infra for this afaik.

[Mario Carneiro]

Why is the syntax not available to the tactic? Isn't this already in the Syntax info? I'm not sure what the state of the rest of the file is, whether it is still unparsed or whether this is being run in the server with a global view.

I am aware we have an MVP implementation, but I would like to see at least one real code action shipping before I'm ready to start building all those other actions

[Mario Carneiro]

I expect that syntax-awareness will need to be solved to do almost any of those actions I listed

[Wojciech Nawrocki]

Mario Carneiro said:

Why is the syntax not available to the tactic? Isn't this already in the Syntax info? I'm not sure what the state of the rest of the file is, whether it is still unparsed or whether this is being run in the server with a global view.

I am aware we have an MVP implementation, but I would like to see at least one real code action shipping before I'm ready to start building all those other actions

The Syntax is already available, the "syntax-aware editing" I was referring to which is not available would be a function Syntax → Syntax → TextEdit which allows you to just modify the Syntax object and gives you the correct string-based edit description. If you can produce the TextEdit manually, all the infra is already in-place (although it has not been stress-tested as you point out).

[Mario Carneiro]

Rather than something that does automatic diffing, I would rather take an AST of the file or part of it, point at a subterm syntax (using e.g. the syntax traverser stuff), and then replace it with a string generated by formatting another syntax that I would like to insert in that location. That would allow us to keep changes localized which is important for any code action. Getting the formatting to match the surroundings is less important, even rust-analyzer isn't that great at this (it relies on rustfmt to pick up the pieces).

[Sebastian Ullrich]

The trouble starts when the changed syntax contains original syntax as well. One tough example I've been thinking about is fusing consecutive if lets into if ... and. There's a big block of existing syntax you don't want to touch there, except you want to re-indent it. Would be much easier if we can just reformat the whole result for sure.

[Mario Carneiro]

I would be okay with completely reformatting the block in that example, at least for V1