lean4

Stream: general

[Chris Hughes]

Just noticed this. https://github.com/leanprover/lean/commit/16f28315eeddf996f85bff96954cd31a94aa4562 Is this something happening imminently or ages away? How badly will this break mathlib?

[Andrew Ashworth]

heh, that's news to me. lean 3 had a good run

[Andrew Ashworth]

if-then-else moves from coercing from Prop to bool to traditional reflection using boolean-valued function

[Andrew Ashworth]

this design doc is very exciting, it seems to hold a lot of improvements for using lean as a programming language

[Patrick Massot]

Can anyone see anything which could be related to using Lean as a proof assistant in this design notes?

[Simon Hudon]

This looks really good :)

[Andrew Ashworth]

no, not in the sense the mathematicians in this channel are using lean, except for scott, since he uses many tactics

[Simon Hudon]

@Patrick Massot Not sure yet. I'll keep poring over it and let you know

[Andrew Ashworth]

obviously all of mathlib is going to break since lean4 isn't going to have an algebraic hierarchy

[Andrew Ashworth]

and that's just one of many big problems

[Patrick Massot]

Moving the algebraic hierarchy from core to mathlib rather sounds like good news

[Patrick Massot]

It was strange to see it in core

[Patrick Massot]

And it currently prevent us from changing anything there

[Andrew Ashworth]

well, i could understand why, having a model of integers and rational numbers is important for computing

[Andrew Ashworth]

it also means Leo is punting on redoing the algebraic hierarchy

[Andrew Ashworth]

ahhh, the new vm is going to support unboxed types...!

[Sebastian Ullrich]

@Andrew Ashworth You seem to have missed the "incrementally rebuild core lib" part :)

[Andrew Ashworth]

i did, but you've been holding out on this important piece of news!

[Sebastian Ullrich]

I did expect someone in here to find it soon enough

[Patrick Massot]

Was it different when going from Lean2 to Lean3?

[Sebastian Ullrich]

We don't want to change the language, esp. syntax, this time (apart from fixing things). I think.

[Patrick Massot]

Would I see any difference then?

[Patrick Massot]

Or is it only about Andrew-syle use of Lean?

[Sebastian Ullrich]

The parser will enable better tooling and mathy notation. Most other things will enable more powerful and faster tactics.

[Patrick Massot]

More math automation?

[Andrew Ashworth]

only if someone like mario or scott decides to write a tactic to do so, i imagine

[Kevin Buzzard]

Is any time frame known for Lean 4?

[Sebastian Ullrich]

Kinda hard to say since we haven't even started yet

[Kevin Buzzard]

So we can at least say that it will not happen, say, within 1 month. Is the idea just to stop working on Lean 3 completely?

[Sebastian Ullrich]

No, we'll probably start on Monday

[Sebastian Ullrich]

:)

[Patrick Massot]

So you finish the monad stuff and stop working in Lean 3?

[Sebastian Ullrich]

I wouldn't expect many new features for Lean 3 at least. Well, the important ones are on the lean4 list anyway.

[Patrick Massot]

How long did it take last time you rewrote Lean from scratch?

[Patrick Massot]

I'm asking only out of curiosity, I'm very very far from having exhausted Lean 3 possibilities for math

[Sebastian Ullrich]

I'd have to check, I didn't participate in the Lean 3 rewrite. I still had a thesis to write in Lean 2.

[Kevin Buzzard]

This is only tangentially related, but would it be possible to get more devs from somewhere? Will MS pay for more? Can people apply for grant money for more? Or is there some problem of the form "Leo doesn't trust anyone enough to mess with his code"?

[Kevin Buzzard]

Also only tangentially related, but is there any chance of some sort of "stable release" i.e. announce that what we currently have is called Lean 3.4?

[Andrew Ashworth]

is that helpful for you if mathlib continues to keep up with nightly lean?

[Sebastian Ullrich]

Yes, there will be a stable release before branching. I don't know if mathlib wants to stick with that or the new nightlies for random bug fixes.

[Kevin Buzzard]

That's great news about the stable release. I will be using Lean as part of my course

[Kevin Buzzard]

in October, and if Lean 4 is still quite chaotic it will be very easy to explain to the students to use Lean 3.4

[Kevin Buzzard]

There is enough in mathlib and Lean 3 for me to be able to do what I want to do

[Andrew Ashworth]

This is only tangentially related, but would it be possible to get more devs from somewhere? Will MS pay for more? Can people apply for grant money for more? Or is there some problem of the form "Leo doesn't trust anyone enough to mess with his code"?

I am curious about how MSR allocates funding for internal projects; I don't know how it works when you're self-funded by a large company

[Moses Schönfinkel]

@Sean Leather Heh... so my comment about Lean4 turns out to be prophetic rather than funny! :)

[Mario Carneiro]

IIRC the lean 3 rewrite took about a year, maybe a bit more

[Mario Carneiro]

The lean 4 plan there is basically the union of all the large scale lean projects currently under consideration. I expect it will take at least 6 months as a low estimate

[Mario Carneiro]

As far as "will it break mathlib", I would say probably yes, but in a good way - moving things out of core lib is music to my ears

[Kevin Buzzard]

I honestly think that writing maths again from scratch might be a lot of fun. I have never seen mathematics grown from the axioms before. There are still huge chunks of mathlib that I haven't read properly. Has anyone in the world read the Matiysevich stuff, for example? I am a number theorist and I know the theory, and I know exactly what the statement of the main theorem is, but I have no idea how he is proving it. Some of the later code looks quite unlike anything I've seen before in Lean. If I had to code up that mathematics it would take me months. Is there a chance that that high-powered stuff will have to be substantially rewritten to port it to Lean 4, or might it just be a case of redoing the basics?

[Scott Morrison]

My very uninformed guess from reading Leo's roadmap is that the high-powered stuff may not actually need a complete rewrite. I'm glad you see it as "an opportunity, not a problem".

[Sean Leather]

Eish! I go away for a few days (family visiting) and return to find the Lean world flipped upside down again. At what point do we get past the always-started-never-finished phase? That is, I've understood Lean 3 to be “experimental” since it began, and now Lean 4 is being started, but Lean 3 never officially dropped the label. Why not just continue incrementally developing Lean 3 using the same goals instead of starting over?

[Patrick Massot]

I don't understand anything about the C++ code of Lean, but I think there is not much news here. We knew big changes were coming (at least #1601, #1674, #1692). I don't see how one could rewrite the parser from scratch without going through an unusable state. So there is clearly a need for a separate branch doing that. Why not calling it Lean4? Also @Sebastian Ullrich told us the syntax should not change much this time. On top of that we learn that Mario and Johannes will be given complete freedom do handle mathlib instead of having some part of it stuck in core lib. It looks like the ideal solution to enjoy the greatness of all those people without the recent tension.

[Patrick Massot]

And we can still use Lean 3 in the mean time

[Sebastian Ullrich]

Well said. Maybe we'll decide to call it Lean 3.5 after all in the end if there aren't many breaking changes

[Sebastian Ullrich]

Though I'm not sure when "let's temporarily shrink core lib" became "let's remove the algebraic hierarchy from core lib forever" :)

[Sean Leather]

@Patrick Massot I have nothing against anything you're saying. I just wonder if it's not possible to remove stuff, rather than start over and add it back. But @Sebastian Ullrich certainly knows better.

[Kevin Buzzard]

@Sebastian Ullrich -- Leo has made it completely clear that he felt that "now" was not the time to be developing mathlib. Of course what he cannot control is the fact that you guys have made a system in which doing mathematics is quite fun, and hence it is simply inevitable that there will be people doing mathematics in Lean. I hope to have students publishing simple papers in undergraduate mathematics journals about how they have used Lean, for example, and this is not going away whatever Leo's opinion is [in fact I think this fits well with Leo's views because Leo likes one-off projects, and writing a small paper saying "this compiles with Lean commit X and mathlib commit Y" means Leo doesn't have to worry about breaking it]. The happy medium which I think we're currently trying to seek is that Mario and his team continue to develop mathlib but (a) try extremely hard not to bother Leo with requests, even reasonable ones such as "please fix ^, it would take 2 minutes" and (b) don't complain when Leo breaks stuff.

[Kevin Buzzard]

On the other hand, if Lean 4 appears with a temporarily-shrunken core lib then I am almost sure that a bunch of people will immediately just add what has disappeared to mathlib and then there's every chance that they will edit it to make it what one might call "better". In my mind there is no doubt that Mario's opinion on how to write a mathematics library is an opinion well worth listening to and to be quite frank I suspect he knows more about this subject than Leo. Or, at least, one might argue that Mario knows how to write a library which mathematicians can use better than Leo does (although this is probably not a question Leo is even interested in).

[Kevin Buzzard]

But at some point the question "is Leo ready for mathlib yet?" will come around again. For example, on the day Lean 4 is released. Will he be?

[Sebastian Ullrich]

I believe the only reason the algebraic hierarchy is in the core lib right now is that it's used by the C++ implementation of norm_num. So yes, in Lean 4 it may actually be realistic to move it to mathlib because it should be possible to build a high-performance norm_num in Lean.

[Simon Hudon]

Regarding the planned change to decidability and ite, are we going to keep dite with access to the assumption that the condition is true / false?

[Mario Carneiro]

The changes to decidable and ite are the ones I am most dubious of. I do not think it would actually be better to define decidable as a bool plus a proof of b = tt <-> p, and the concerns that make this reasonable in Coq don't apply directly in lean (in particular because we don't use kernel computation as much). For ite, we already have cond, ite and dite and these three functions are needed regardless of any notations attached to them. But I don't see any obvious alternate way to interpret if h : p then t else e other than using dite, and anything that uses bool here will be too cumbersome. For the nondependent if p then t else e, it's not really a big deal if this is interpreted as cond or ite, but there should not be any relative performance penalty between the two in any case, and if there is this is a fault of the code generator not the functions.

[Mario Carneiro]

Note: if you want to write a decidable p program by defining a bool program and prove it is correct, you can do this by using decidable_of_iff (my_bool = tt <-> p) <proof> with essentially no performance penalty. There is no need to change the definition for this.

[Simon Hudon]

In this situation, I think we can identify two changes: ite taking a bool instead of a decidable proposition and decidable being redefined. I think regardless of the definition of decidable, we can keep if _ then _ else _ the same. In the non dependent case, I can see how a boolean condition would make the condition easier to rewrite.

[Moses Schönfinkel]

Coq is a lot more cumbersome in this regard. You end up writing something like if Z_lt_dec a b instead of if h : a < b; the later is naturally a lot more readable (where Z_lt_dec is unsurprisingly something like {a < b} + {~a < b} which is just Coq notation for sumbools). There is a weird notation-al dissonance between props and their "boolean" (decidable) alter-egos in Coq

[Simon Hudon]

Yeah that's true. It's a really cool thing about Lean. It seems like just writing an obvious program is so much easier and that way of defining if _ then _ else _ has something to do with it.

[Moses Schönfinkel]

Notation is just too important, regardless of the amount of bikeshedding blame ending up being bestowed upon those partaking in the discussion :P. (I guess Iverson would agree!)

[Moses Schönfinkel]

Which is twice as amusing because then what on Earth was he thinking with APL.

[Simon Hudon]

That's what I was about to ask. I only know Iverson from APL and APL is only an example of how to make a miserable mess of your syntax

[Moses Schönfinkel]

Well his Turing award lecture was named Notation as a tool of thought so one would think that he of all people would understand the importance.

[Moses Schönfinkel]

And then he goes on to explain what makes good notation with some very valid points.

[Moses Schönfinkel]

And then he proceeds to use APL to demonstrate those valid points and at this point everyone is like "are you serious?".

[Simon Hudon]

Interesting. I haven't read it. I'll have a look.

[Simon Hudon]

My reference for mathematical notation is Dijkstra and his idea of "letting the symbols do the work"

[Moses Schönfinkel]

I have mixed feelings about DIjkstra ^^.

[Simon Hudon]

He wrote a note on his notational choices in EWD 1300: https://www.cs.utexas.edu/users/EWD/index13xx.html

[Moses Schönfinkel]

Why am I not one bit surprised that it's hand-written. He would also write computer programs in English... argh! :)

[Simon Hudon]

Yeah you can take all his opinions as holy writ. What bothers you in his ideas?

[Simon Hudon]

:D

[Simon Hudon]

I love his handwriting :D

[Moses Schönfinkel]

It's more like his personality and actions not coinciding with what he actually says.

[Moses Schönfinkel]

For example "the humble programmer".

[Moses Schönfinkel]

Humility was probably his weakest point :P.

[Simon Hudon]

Haha! Yeah but the humility he speaks of in that is something he did: he did assume his problems were too hard to just approach head on so he worked on reducing their intellectual demands

[Moses Schönfinkel]

Have you seen his correspondence with Backus? For some reason my personal feelings towards Dijsktra make me like even his ideas less :(.

[Simon Hudon]

No, where can I find it?

[Simon Hudon]

By "his ideas" do you mean Backus?

[Moses Schönfinkel]

Nono, I mean Dijsktra.

[Moses Schönfinkel]

https://medium.com/@acidflask/this-guys-arrogance-takes-your-breath-away-5b903624ca5f

[Moses Schönfinkel]

Backus would talk about functional programming and liberation from von-neumman architecture and thinking in bytes.

[Moses Schönfinkel]

And Dijstrka would unleash a flurry of what is difficult to describe :).

[Moses Schönfinkel]

It's a fairly long chain of replies tho, which makes me dislike Dijsktra from a really silly personal standpoint.

[Moses Schönfinkel]

Putting personal feelings aside tho, objectively Dijsktra was an excellent computer scientist.

[Simon Hudon]

That's interesting. I started off taking Dijkstra's word as holy gospel and followed his approach for my master's. It's been very enlightening for me to learn to disagree with him and to stop tearing down projects that I would not personally undertake

[Simon Hudon]

Specifically, I had to eventually dismiss his "Computer Science is no more about computers than astronomy is about telescopes" comment. Z3 is actually what led me there. Having fast computers makes such a difference in building large formal proofs. I had to rethink my views in the field

[Moses Schönfinkel]

I think we also often somehow disregard that there exist proofs that are "computational" in their nature, which the 4-colour theorem is a prime example of. I am guessing they arise when your "domain" is constrained but still colossal.

[Moses Schönfinkel]

But perhaps Kevin or Patrick would be of different opinion.

[Simon Hudon]

That kind of proof still bother me a bit. I think they are a valid certificate for their claim but I wonder if they limit the amount of insight that one can gain from reading it.

[Moses Schönfinkel]

Does an alternative that doesn't need to check <many> cases exist yet?

[Kevin Buzzard]

Nope, not as far as I know.

[Kevin Buzzard]

Although I think <many> went down from the original 2000 or so

[Simon Hudon]

Not that I know of. My point is that I'm hesitant to accept the computational nature of the proof. I'm not sure how useful that particular fact is but a proof that is inscrutable proves one fact but if the proof can show people how to do mathematics or computer science, it does so more to advance the field. Admittedly if the theorem is referenced all the time but the proof is uninteresting, it still moves the field forward

[Kevin Buzzard]

I don't know much about proofs which are computational in nature, the proofs I know are all about building elaborate structures.

[Moses Schönfinkel]

This particular theorem is super-interesting!

[Simon Hudon]

How enlightening was the proof for you?

[Moses Schönfinkel]

Not one bit.

[Simon Hudon]

What is so interesting about the theorem?

[Moses Schönfinkel]

Its applications. People optimize compilers with it, people use it to cover areas with signal with it. It's a useful, therefore interesting??? theorem.

[Moses Schönfinkel]

It's not some claim about perfectoid spaces :P.

[Simon Hudon]

I was not aware of that. That's pretty cool :) Do you know how it helps with compilers?

[Moses Schönfinkel]

I think something to do with assigning variables to registers.

[Moses Schönfinkel]

To avoid spilling perhaps?

[Moses Schönfinkel]

@Simon Hudon At one point in the past Kevin told me he's not very fond of proofs that rely purely on human understanding of the world (such as commutativity of multiplication being explained "geometrically" by counting soldiers rows first / cols first and noting that their number doesn't change) - any observations in this regard?

[Simon Hudon]

That makes sense. I'm still not sure where the planarity of the graph intervenes though

[Andrew Ashworth]

the trouble is intuition will only get you so far, and that's why appeals to informal proofs like counting soldiers is not ideal

[Moses Schönfinkel]

That's a similar argument to Kevin's. I just wonder if you would accept "simple" proofs like that as proofs.

[Moses Schönfinkel]

Lean would of course not.

[Simon Hudon]

Interesting, yes I do. I don't like proofs by analogy, not in technical texts anyway. I have no problems with proofs that purely shuffle symbols around. But I like them to be arranged in way that is obvious so that most of the proof is of the sort "there is only one thing you can do now" with as little surprises as possible. To me, it boils down to this: do you want to impress your audience or do you want to teach them something beyond this particular fact.

[Moses Schönfinkel]

But it's still a proof... for a human, right?

[Andrew Ashworth]

i would prefer something that does both? a well written paper interspersed with reasoning and formal proof

[Moses Schönfinkel]

If I were to tell you that you can count soldiers from "either perspective" to get the same result, would you be convinced that this is the case for an arbitrary number of soldiers?

[Moses Schönfinkel]

How would one formulate this kind of proof in Lean?

[Simon Hudon]

But it's still a proof... for a human, right?

Yes exactly. So you should have a calc block that spans pages and pages even if it's valid. You're losing people's attention. On the other hand don't, for the sake of being intuitive, jump into the rabbit hole that is the breaking down of equivalences into mutual implication or the analysis of multiple cases. I like efficiency in (human) formal reasoning

[Simon Hudon]

How would one formulate this kind of proof in Lean?

I wouldn't even try but I'm curious about what you'd come up with

[Moses Schönfinkel]

I am not sure. In general, if I were to call this a "geometrical proof", how would one begin in a mechanized / formalized setting.

[Simon Hudon]

I would venture the opinion that it is impossible because its justification is not in any set of axiom but in an experience of space that is common to most humans.

[Kevin Buzzard]

I think the only proof of the "counting soldiers in a rectangle" which I can accept is induction on one of the sides. I was ranting about this in the finite sequences thread though -- I don't know whether the statement "partition X into m disjoint subobjects each of size d -> size of X is m*d" should be a theorem about finite sets, finsets or fintypes. In reality it's a theorem about objects in a rectangle

[Simon Hudon]

And it is a big weakness. It's a bit of stage magic: you make it appear like you solved the problem but the only criterion is that "people agree"

[Moses Schönfinkel]

Sounds very reasonable. Could one formulate a model of such intuitive understanding that would be consistent with our perception thereof? Like ZFC but... with more hand-waving :P.

[Kevin Buzzard]

and I think it's a bit weird that one theorem in maths / reality threatens to become three in Lean.

[Moses Schönfinkel]

Right. But that's what proofs are, by definition. "People agree."

[Kevin Buzzard]

Not any more.

[Kevin Buzzard]

Not in mathematics.

[Moses Schönfinkel]

It's not?

[Moses Schönfinkel]

Oh, nice.

[Kevin Buzzard]

I think it's going too fast. That's why I'm here.

[Kevin Buzzard]

I think what is commonly accepted as a proof in mathematics is "the experts look at the techniques and figure that they should be enough"

[Moses Schönfinkel]

Ufffff...

[Kevin Buzzard]

and then the rest of the people just say "well the experts seem to believe it"

[Simon Hudon]

I would venture the opinion that it's moving towards "people agree on a fixed number of rules and once they agreed, you have to decide whether the rules have been followed"

[Moses Schönfinkel]

That doesn't sound reassuring.

[Kevin Buzzard]

Patrick goes on about Scholze. But the number of people who have read all of his recent work is probably 0 (other than Scholze) now, because he's been branching out a bit. On the other hand, he has form, and some people have checked some of his stuff very carefully

[Kevin Buzzard]

so there's a certain amount of trust involved.

[Kevin Buzzard]

But he is not perfect even though he's a genius, and this is what makes me scared.

[Kevin Buzzard]

because mathematics is being done at a ludicrously quick rate at the minute, with it being so easy to knock up a pdf and stick it on ArXiv

[Moses Schönfinkel]

Of course there's "perfectoid space" on Scholze's wiki page.

[Moses Schönfinkel]

So I guess you guys are, and this is a terminus technicus, "in a pickle".

[Moses Schönfinkel]

Checking proofs is apparently hard.

[Kevin Buzzard]

Well, I think that people don't think we are in a pickle.

[Kevin Buzzard]

and I am kind-of concerned that we might find out too late that some important thing was wrong and then everyone will have egg on their face.

[Mario Carneiro]

Here's my kind of formalization of soldiers-in-a-rectangle proof of commutativity:

• Why should we believe that counting from one direction or another should give the same number?
  • because it's the same soldiers
• But why should counting the same soldiers in a different order give the same number?
  • Because that's what we mean by the "same number" (alternatively, you can push on this intuition but I will stick to conventional cardinality)
• But how do we know we aren't double counting or something? That would clearly mess up the count
  • Because we are sweeping from one side to another in the count in some definite order, which prevents a double count

At this point, I see the formal proof clearly: it is a bijection between fin m x fin n and itself that counts lexicographically in two different ways

[Kevin Buzzard]

On the other hand I am open to the opinion that I am just getting old. I am happy that FLT is proved but then again I had time to read the proof (I was a post-doc and it was in my area so I had to read it). But ever since then I've felt less and less convinced that people have been checking all the details of absolutely everything, however perhaps I'm just more paranoid and slower now.

[Kevin Buzzard]

Meh but when you write down the bijection between fin m x fin n and fin (m x n) ... oh no you're right, you don't seem to need induction!

[Kevin Buzzard]

But now you have to prove that if fin x and fin y are in bijective correspondence then x=y.

[Kevin Buzzard]

Mario's proof is the categorification proof. Don't prove a * b = b * a in nat, prove A x B bijects with B x A in the category of sets.

[Simon Hudon]

I'm just more paranoid and slower now.

That sounds like a good thing to have in an audience. If the smartest of the smart are the ones reviewing the FLT proof, what will be left of that understanding once those people will have died? Will you need people dedicated to learning and understanding that particular proof and transmitting that understanding from generation to generation?

[Moses Schönfinkel]

Remember Fermat had a beautiful proof that just barely didn't fit the margin in his notebook or what was it ;). Surely we can easily understand 17th century mathematics!

[Simon Hudon]

I think that's mathematician code for "... and then magic happens ..."

[Moses Schönfinkel]

What sounds better is: Magician's code for "... and then mathematics happens ...".

[Moses Schönfinkel]

Oh man, I'll be getting like 4 hours of sleep. Yey... off to bed, nite.

[Mario Carneiro]

But now you have to prove that if fin x and fin y are in bijective correspondence then x=y.
Mario's proof is the categorification proof. Don't prove a * b = b * a in nat, prove A x B bijects with B x A in the category of sets.

The goal with that proof was to try to establish what formal proof underlies the confidence in the result given from the "geometric proof" of this theorem. But most of this is actually just pinning down what we mean when we say things. When I say there are 10 soldiers in a line, what does that mean? I guess I should be able to count up 10 times while naming the soldiers, but then 10 is defined in terms of itself which isn't good. Perhaps we have some internal conception of 10 as a number, and then we map this internal representation onto the soldiers; in that case it looks like we're talking about bijecting our set A of soldiers with fin n where n : nat is our abstract conception of numbers.

So where is fin n = fin m -> n = m hiding? I would argue it is in the intuitive notion that there are a well defined number of soldiers in the line in the first place, which is generally unchallenged. One may worry at this point that this is an empirical fact, that it just so happens that in our universe every time we count the same thing twice we get the same number (which obviously is false for a variety of reasons like miscounting), but we can push the theorem back to the platonic realm by counting our own abstract numbers, i.e. forming a bijection {1,...,n}->{1,...,m} and showing that always n=m in this case.

[Moses Schönfinkel]

^ This follows the "intuitive" notion of how cardinality is extended beyond finite. Just form a bijection with something nice (such as natural numbers) and then put your faith in the nice set.

[Moses Schönfinkel]

I really need to sleep. Bai.

[Sean Leather]

Some questions on the design notes:

if-then-else using bool instead of Prop. As soon as we started programming with Lean (version 3), it became clear that if-then-else with Prop creates more problems that it solves.

Can anyone elaborate on the problems created?

The elaborator already has support for a coercion from Prop to bool (for decidable propositions). The dependent if H : p then t else e may look cute, but it is unnecessary now that we have match.

Doesn't the “now that we have match” statement apply equally well to the non-dependent if-then-else? Stated another way: why would you want if-then-else for non-dependent propositions if you don't want if-then-else for dependent propositions? (I'm not arguing one way or another, just trying to understand the logic.)

[Simon Hudon]

I'm worried about those statements too. I wouldn't want to see those two if-then-else- disappear. More worrisome still is the introduction of match in the expression language. In Coq, they tend to make expressions larger than necessary. I really like that we're using auxiliary definitions instead

[Sebastian Ullrich]

Uh? There is no planned change to match.

[Simon Hudon]

Glad to hear it! So what does Leo mean what he says those things?

[Joe Hendrix]

In the "SSA or SIL" question in the design notes referring to LLVM IR vis Swift IL?

[Mario Carneiro]

SIL indeed stands for swift IL, SSA is static single assignment form in general. I think LLVM is off the table now

[Simon Hudon]

I think LLVM is off the table now

Yes? What disqualified it?

[Mario Carneiro]

It's very complicated with its own gotchas, and it's unlikely to produce better results than just having our own IL

[Mario Carneiro]

Leo works with Nuno Lopes, who has done formalization of LLVM and I think is the source of this view

[Simon Hudon]

That's interesting. I thought having that kind of formalization might be a good reason to use it

[Mario Carneiro]

I think it's more like once you've formalized a big language you know all the little suboptimalities in it. Like how I now have a better understanding of lean's theory to see why non-transitive definitional equality is a problem

[Mario Carneiro]

plus we're not talking a formalization in a proof assistant, I think it comes in the form of papers and compiler optimization checking tools

[Simon Hudon]

Ah ok. I thought you were talking of someone from the Vellvm project

[Joe Hendrix]

If you target Swift IL, then you are implicitly saying that you are fine with LLVM IR since SIL is translated to LLVM.

[Mario Carneiro]

I think it's just being used for inspiration

[Joe Hendrix]

GHC's compilation is essentially "System F core -> STG -> Cmm -> (native | LLVM)". I would expect a similar flow would work well for Lean.

[Simon Hudon]

@jhx Do you think it will be problematic to use Haskell techniques in Lean even though Lean is strict by default?

[Joe Hendrix]

It's true. I could imagine Lean maps a system F like core directly to a low-level Cmm representation. My understanding is that STG is provides a uniform closure representation and is where strictness analysis is performed prior to Cmm generation.

[Johannes Hölzl]

Glad to hear it! So what does Leo mean what he says those things?

Leo didn't write to get rid of match, in the (unpolished) document he writes that dependent if-then-else(dite) is not necessary anymore due to having match now. But I hope that we can implement if h : p then a else b with the parser in Lean4 ourself.

[Mario Carneiro]

I don't understand that comment either. AFAIK lean has had match since lean 1, what's new?

[Johannes Hölzl]

My guess is that in later Lean versions match got improved support for the dependent case? But I also don't see how match should replace the dependent if case. The later also includes the construction of the decidable predicate.

[Joe Hendrix]

Assuming the decidable changes are implemented, should the h in if h : p then a else b syntax ensure h has type p (resp. not p)? That syntax would then hide the underlying representation choice.