Web Programming with Lean 4

Stream: lean4

[Tom Houlé]

I have been working with rust for a long time, currently I am using Lean (3) as a tool to learn more maths, and I have to say the perspective of Rust <-> Lean 4 interop is extremely exciting — you could do things like embed wasmtime as a library, or get a mature regex engine "for free" by wrapping the regex crate. I haven't looked into that in depth yet, but an ergonomic bindgen-style crate could be possible. The fact that the Lean 4 objects are reference counted should make this easier.

[Uranus Testing]

If you interested, you can look at example of connecting libwebsockets (C-library, which also provides some kind of web server) to Lean 4 via FFI: https://github.com/o89/n2o. Connecting Rust-libraries shouldnʼt be harder, I guess.

[Jannis Limperg]

Henry Story said:

Also am very intrigued by what the future holds for programming using proof assistants, especially with HoTT allowing one to transport proofs between types. As I am building a security platform, being able to produce proofs of the correctness of the code, would be very advantageous.

Worth noting, then, that Lean is explicitly HoTT-incompatible. However, I suspect that HoTT or no HoTT wouldn't make much of a difference for whatever proofs you want to do.

[Henry Story]

Thanks @Jannis Limperg. Is it still true that Lean4 maintains HoTT incompatibility? As I understood from watching a few videos Lean4 is very extensible... (I have no idea of what would be needed to add such a feature to Lean4).
The interest of HoTT as I understand is that one could say prove something on a simple data structure (say 0 and succ for Nat) and transport the proofs to another more complicated type (eg binary numbers). I could see that being useful in many places, such as proving things on simple representations of RDF say and then transporting those findings to more efficient representations (perhaps B-Trees or what not).

[Mario Carneiro]

You don't need HoTT to do that

[Henry Story]

Ah it is the main example of this article on Cubical Agda. It may be that I oversimplified the story of the benefits to be gained.

[Henry Story]

Mind you, that is really looking a few (very large) steps ahead of where I am :-)
For the moment I guess I'd first be interested to see where it would make sense to use Lean4 as a programming language. Perhaps everywhere? I mean could one even envision writing a web server with it? (or does that require codata?). But perhaps everywhere eventually, but initially most useful for working with ... ?

[Jannis Limperg]

The HoTT issue is about the core type theory of Lean, which assumes an axiom that contradicts HoTT. So afaict, Lean 4 will always remain HoTT-incompatible. (I'm not 100% sure what happens if you define an equality type in Type, not Prop, and axiomatise univalence for this type.)

Wrt practical uses of HoTT, it is still unclear to me whether it really helps or mostly shuffles proof obligations around. I did one project using HoTT (axiomatised in Agda) where I saw clear benefits but also had to do some nasty HoTT-specific proofs. In any case, I would expect that any practical development using HoTT could also be done without it, with at most a moderate increase in boilerplate.

Wrt suitability of Lean as a general-purpose programming language, I don't think anyone except Joe and his team has any practical experience, so it's hard to tell. I'm pretty sure, though, that the lack of codata is not a major limitation. If you need a program that runs indefinitely, you can just write a partial main loop that calls your request handling code, and each request is handled by a finite computation. More generally, you can work in a partiality monad and use a partial interpreter for that monad, though this may introduce some overhead.

[Gabriel Ebner]

Whenever HoTT is mentioned here I have to shamelessly promote https://github.com/gebner/hott3
It is possible to formalize HoTT in Lean 3, but of course it doesn't integrate with mathlib (which is probably impossible no matter how you do it due to mathlib's extensive use of choice). The same approach to formalize HoTT also works in Lean 4 (and maybe even nicer because you can change the syntax).
That said, HoTT in Lean 3 never really took off and it hasn't advanced beyond a proof-of-concept stage. If I wanted to formalize something in HoTT, I'd rather look into the cubical system du jour.

[Kevin Buzzard]

My experience with HoTT in undergraduate or MSc level pure mathematics (and my comments are restricted to this domain) is that it looks like it promises much, but doesn't actually deliver. I know of one example where it would help, and several examples where it looks like it will help but probably won't help. I have never used a HoTT system seriously and my main concern is that there might also be several examples where it actively hinders. Nothing like mathlib has been developed in any HoTT system, which one might want to take as evidence that it can't be done, but having talked a lot to HoTT people my impression is that the main reason there's no HoTT undergraduate maths library is that there are many foundational questions regarding HoTT which are regarded as fashionable (e.g. work on cubical), and so people in HoTT tend to work on those questions -- they regard formalising undergraduate and MSc pure mathematics as pointless, in the main.

Let me first start by explaining the example I know where it would help. A _local ring_ is -- it doesn't really matter what it is, it's a ring which satisfies some axioms. It's a theorem that if R is a local ring and S is a ring which is isomorphic to R, then S is also a local ring. I have asked many mathematicians how to prove this, and some are able to sketch a proof, but some just look at me like I'm an idiot and say that there is nothing to prove (this is a completely consistent viewpoint within mathematics departments -- all predicates we consider are isomorphism-invariant; a predicate which isn't isomorphism-invariant would just die out in the mathematics ecosystem). In a HoTT system there is nothing to prove: R is isomorphic to S, so R equals S, so done. In a non-HoTT system like Lean we have to build this proof. However the proof is mechanical -- a ring is local if it has a unique maximal ideal, which is just some predicate on the lattice of ideals of the ring, so you have to check that isomorphic rings have isomorphic lattices of ideals, that sort of thing.

Now here's another example, which looks very similar. Say X is a compact topological space, and Y is a topological space which is homeomorphic (i.e. isomorphic as a topological space) to X. Prove that Y is compact. Again this is immediate in a HoTT theory. But there is a more general theorem here: if X is compact and X -> Y is a continuous surjection (a condition weaker than a homeomorphism) then Y is compact. This can't be proved for free, and should be in any decent maths library. The original assertion, that Y isomorphic to X is compact if X is, follows immediately from this. This is an observation of Mario, and ever since I internalised it I've always looked out for examples of when mathematicians want to transfer structure along isomorphisms, and in a surprisingly large amount of cases this transfer can be done just using more general results in the API. In fact it's worth revisiting the local ring example above. If we have a surjective ring hom R -> S from a local ring R to a ring S then S is either local, or the zero ring. So there is a (weird to mathematicians, but apparently helpful here) predicate on a ring of being "pre-local", which means "either a local ring, or zero" (a bit like "either a prime, or 1"), and if R is prelocal and R -> S is surjective then S is pre-local, something which one could imagine in a maths library, and so to transfer locality one just has to check that if R is non-zero and isomorphic to S, then S is non-zero, which is easy. This rather weakens (for me, at least) the argument that we should be (a) using HoTT to do this kind of mathematics or (b) making a tactic which transfers isomorphism-invariant predicates (e.g. any predicate which comes up in mathematics, such as local or compact).

The second instance where I've seen HoTT people telling me "this would be easy in HoTT" is an example where I recently discovered (when writing https://arxiv.org/abs/2101.02602 a couple of weeks ago) that actually I no longer believe the claims of the HoTTers. I give more details in section 3.4 of the paper but here's the gist of it. Say I want to prove that a map A -> B satisfies some predicate (in the actual example I have a pair of maps A -> B and B -> C and want to prove that the pair satisfy a predicate, but let's drop C and just consider A -> B because the point I'm trying to make remains). I have in my possession rings A' and B', a map A' -> B', proofs that A' and A are isomorphic and that B' and B are isomorphic, and a proof that the map A' -> B' satisfies the predicate. To prove that A -> B satisfies the predicate in Lean I had to check that this predicate transferred over isomorphisms (which was a small amount of work) and also that the commutative square [a square with A -> B on the top, A' -> B' on the bottom, and isomorphisms A -> A' and B -> B' on the sides] commutes (this was a larger amount of work). The problem superficially looks like it is one which HoTT could help with, but I am no longer so sure. I think classical HoTT really could not help at all. We know A=A' and B=B' but we do not know that the maps A -> B and A' -> B' are equal, and in a HoTT theory my impression is that if you use univalence then you will not be able to prove this, because you will transfer the A' -> B' map which satisfies the predicate into some map A -> B' which you know satisfies the predicate but which you can't compute with, as you've used an axiom to construct it, so you can't show it equals your original map A -> B. The point is that the commutativity of the diagram is a theorem, not something which comes for free. With cubical you'd be able to construct a map A -> B which has the property and which you can compute with, but then you still have to do the computation to prove it's the map you're interested in, which boils down to checking the diagram commutes anyway. In the schemes work we solve this problem by using the fact that A -> B comes from a universal property which we show also holds for A' and B' and then the proof becomes rather conceptual; the proof that A' -> B' has the property just compiles equally well to also prove that A -> B has the property.

In short then, within the domain of undergraduate and MSc mathematics I cannot yet see a useful application of HoTT which we can't get relatively straightforwardly in Lean, and furthermore I do not have much evidence for the assertion that there will be no hidden extra difficulties in making a HoTT library containing the kind of material which is in mathlib -- I am concerned that rfl will be highly degraded in a HoTT version of mathlib, and we use rfl a lot in mathlib. The reason I'm interested in making an UG maths library in a theorem prover is that it's something which mainstream mathematicians seem to be able to identify with, which is more than can be said for the HoTT theory right now; my impression is that in mathematical circles the achievements of the HoTT people are really regarded as foundational and hence "not really proper mathematics" in some sense. Of course, as a "proper mathematician" I am offering a perhaps rather biased viewpoint, so some of what I've said should be taken with a pinch of salt perhaps.

[Henry Story]

Thanks very much for the detailed answer @Kevin Buzzard . It will take me a long time to digest your answer, especially as I now have to reduce my time exploring Category Theory, which I came across programming the semantic web and go back to working on the access control layer of Tim Berners-Lee's Social Linked Data Server.

It don't really know how far the mathematics of undergraduate and MSc level Math students compares to the mathematics we are using in programming languages (mostly with little knowledge of the theory). I went to a course by Abbas Edelat in 1994 on Category Theory at Imperial College but could not understand what was going on (I was also short on time). It is only when I started programming Scala 15 years later that I came across them explicitly. There I found some very interesting uses of Free Monads, leading me to wonder how the notion of context that they bring in might be related to Modal Logics which I knew through careful studying David Lewis as an undergraduate). Somehow I ended up back at university which gave me time to explore these things, and I found that indeed Indexed Strong Monads are related to modalities useful for Security Reasoning.
Another example is the now very popular Rust programming language which is based on work on Linear Logic and later studied in Category Theory by people like Samson Abramsky. When I first came across Linear Logic 3 years ago, I had no idea what to make of it. It is only when I saw how it was applied in Languages such as Idris2 and Granule -- which has Linear Graded Modal Types (see talk) -- that I could see how it could be interpreted. Linear types allow one to write code with the efficiency of C, no garbage collection, but without the constant danger of resource (memory, sockets, etc.. leakage). Now whole ecosystem of programmers are using linear logic happily every day, and being surprisingly productive doing.
So I it is quite possible that HoTT (and the recent work on Modal HoTT) will have very interesting applications to programming. Even without HoTT I'd be happy to see a few more examples of programs written in Lean4 in areas I understand, to see how I could use it.
(Btw. I think for an (under)graduate course in Mathematics you made a good choice with Lean, as it does have a very clean environment to allow students to step into. Agda would have required those students to learn Emacs, where I think you would have lost most of them. That is being improved.)
I guess as I have a programming background, I am always interested to see what tools are available, and how and where they would be usefully applied, so that I can understand when to reach for them. I have only 2 months experience working with Agda, but none yet compiling it to something I could use in an application I need. But I can see that the future of programming is mathematics :-)

@sci_tec @dorchard @smdiehl @buggymcbugfix @heades A talk on Granule, a functional programming language with linear and graded modal types using (co)monads for fine tuning of (co)effects given at this summer @typelevel summit organised by the #Scala community. See https://www.cs.kent.ac.uk/people/staff/dao7/publ/granule-icfp19.pdf https://portal.klewel.com/watch/webcast/typelevel-summit-lausanne-2019/talk/4/

- The 🐟‍‍ BabelFish (@bblfish)

[Riccardo Brasca]

What happens in HoTT to statements that are not isomorphism-invariant? I guess that one simply cannot write them, but does this mean that stating a theorem is more difficult in HoTT than in (say) Lean? I mean, the fact that being a local ring is preserved by ring isomorphisms is trivial, but it still is a mathematical statement.

[Riccardo Brasca]

Maybe I am being completely naive, but I find it surprising that one can prove this literally without doing anything

[Adam Topaz]

You can write them, but you can't prove equality.

[Adam Topaz]

Concerning Kevin's example with algebras (i.e. morphisms of commutative rings $A \to B$), if I understand correctly, you can still make it work in the following way. You can define some structure which consists of the data of $A$, $B$, and the morphism $A \to B$. You can define isomorphisms between two such structures in the usual way, and prove that isomorphic terms are equal, hence you can rewrite along such an equality. But like Kevin mentions this doesn't "save" any work, since you still have to prove something about the commutativity of the diagram involved at some point. You just moved the proof somewhere else.

[Riccardo Brasca]

I mean (ridiculous) statements like $3 \in R$, where $3$ is the integer $3 \in \mathbf{Z}$. This is true for $R =\mathbf {Z}$, but false for $S = \mathbf{Z}[X]/X$, even if $R \cong S$. Of course this is a statement that is completely irrelevant mathematically, but still...

[Riccardo Brasca]

I apologize if I am writing total nonsense :innocent:

[Adam Topaz]

Take a look at the cubical agda librrary where they prove that isomorphic rings are equal:
https://github.com/agda/cubical/blob/390ac95aa2f87a131844aabe20a7b3ed81d608f4/Cubical/Algebra/Ring/Base.agda#L232

[Adam Topaz]

What is the actual proposition $3 \in R$?

[Riccardo Brasca]

I admit I don't know how to write it in Lean (in my set-theoretic mind $3 \in R$ is a proposition, it means the $3$ is an element of the set $R$, this can be true or false).

[Adam Topaz]

But what is 3?

[Riccardo Brasca]

The integer $3$, $1+1+1$ or whatever you want. But in any case, non isomorphism-invariant statements do exist, right? If $P$ is such a statement that hold for $X$, where $X$ is "something$$ but doesn't hold for some $Y$ with $X \cong Y$, it is surprising that we can consider $X=Y$ (since, I believe, one of the properties of $=$ that we want is that if something holds for $X$ and $X=Y$ then the same thing holds for $Y$)

[Riccardo Brasca]

In real world mathematics what we usually don't say, but use all the time, is that all our statements are isomorphism-invariant, so this doesn't matter

[Riccardo Brasca]

Agait it is very possible that this is completely nonsensical

[Johan Commelin]

The trick in HoTT is that you can just transfer $3 \in R$ to $3 \in S$ along the isomequality...

[Johan Commelin]

so even "non-isomorphism-invariant" props are just beaten into isomorphism-invariant shapes...

[Johan Commelin]

It is just that the $\in$ in $3 \in S$ no longer means what you think it does...

[Adam Topaz]

Yeah, in HoTT there is no statement which is not "equality invariant", but there are some things you can call "isomorphic" which you cannot prove are actually "equal"

[Jannis Limperg]

Kevin Buzzard said:

I have in my possession rings A' and B', a map A' -> B', proofs that A' and A are isomorphic and that B' and B are isomorphic, and a proof that the map A' -> B' satisfies the predicate. To prove that A -> B satisfies the predicate in Lean I had to check that this predicate transferred over isomorphisms (which was a small amount of work) and also that the commutative square [a square with A -> B on the top, A' -> B' on the bottom, and isomorphisms A -> A' and B -> B' on the sides] commutes (this was a larger amount of work). The problem superficially looks like it is one which HoTT could help with, but I am no longer so sure. I think classical HoTT really could not help at all. We know A=A' and B=B' but we do not know that the maps A -> B and A' -> B' are equal, and in a HoTT theory my impression is that if you use univalence then you will not be able to prove this, because you will transfer the A' -> B' map which satisfies the predicate into some map A -> B' which you know satisfies the predicate but which you can't compute with, as you've used an axiom to construct it, so you can't show it equals your original map A -> B.

You are right that HoTT does not help you here, but it does not hinder either. Say you have an iso i : A ~= A' and you use univalence to turn this into an equality e : A = A'. This induces a map transp e : A -> A', the 'transport' of e. Then the univalence axiom also implies that transp e = i. In a cubical type theory, this equality is definitional, but even the propositional version should suffice for whatever you want to do.

Riccardo Brasca said:

In real world mathematics what we usually don't say, but use all the time, is that all our statements are isomorphism-invariant, so this doesn't matter

In a type theory which is consistent with HoTT, statements which are not invariant under isomorphism cannot be expressed. Otherwise the type theory would not be consistent with HoTT since, as you note, we would have P X and X = Y but not P Y. This is one of the major differences between set theory and Martin-Löf type theory.

[Adam Topaz]

I think an interesting example is the type of degree $37$ extensions of $\mathbb{F}_5$. As a homotopy type, this is $B(\mathbb{Z}/37)$, and any two terms of this type are isomorphic as fields.

[Riccardo Brasca]

It seems a little bit some kind of black magic, but also type theory was confusing at the beginning...

[Kevin Buzzard]

Riccardo I remember being confused by all of this a couple of years ago. I've just seen sufficiently many examples to make it not confusing any more. Your $3\in R$ thing doesn't make sense because every term has exactly one type -- type theory stops you making a lot of non-isomorphism-invariant statements. On the other hand you might be surprised to know that $\mathbb{N}=\mathbb{Z}$ is unprovable in Lean. The reason for this is that it could easily be true! You could just define int to be nat and put a new addition on it. But we don't do it like that, so it's unprovable.

[Riccardo Brasca]

I think I got the point, but just to make an example taken from real mathematics: let us consider the category of metric spaces and continuous functions. The statement "$(X, d_X)$ is bounded" is now a completely legitimate proposition. But now we can have $(X, d_X) \cong (Y, d_Y)$ in our category, with $(X, d_X)$ bounded and $(Y, d_Y)$ unbounded.

[Kevin Buzzard]

I don't know much about HoTT but presumably what's going on is that being bounded is a predicate on metric spaces, and an isomorphism of metric spaces will be distance-preserving -- an isomorphism will by definition preserve all structure. Your isomorphism is an isomorphism of topological spaces but boundedness doesn't make sense on topological spaces

[Kevin Buzzard]

Given a random structure you don't get a category because you can't work out what the morphisms are, they're not intrinsic to the structure. But there is a notion of isomorphism which is intrinsic to the structure and it's an equiv which literally maps the fields to each other.

[Adam Topaz]

Yes exactly. To get an equality of metric spaces for an isomorphism you need the isomorphism to be distance preserving. It's not enough to have a homeomorphism on the topological spaces. On the other hand, homeomorphic topological spaces are equal.

[Riccardo Brasca]

Aah, isomorphism doesn't mean isomorphism in some category I can play with, it is something formal given by the structure itself. Now it's clear, thank you!

[Kevin Buzzard]

You have put a standard category structure on metric spaces but this is not intrinsic to the type, like continuous maps are not intrinsic to topological spaces -- they are no more canonical from the type theory point of view than the category of top spaces with open, possibly discontinuous, maps as morphisms. Mathematicians just use the idea which turned out to be useful. In my research I once had to consider a category of metric spaces but with distance-nonincreasing maps as morphisms.

[Bhavik Mehta]

Kevin Buzzard said:

You have put a standard category structure on metric spaces but this is not intrinsic to the type, like continuous maps are not intrinsic to topological spaces -- they are no more canonical from the type theory point of view than the category of top spaces with open, possibly discontinuous, maps as morphisms. Mathematicians just use the idea which turned out to be useful. In my research I once had to consider a category of metric spaces but with distance-nonincreasing maps as morphisms.

On top of this, this latter category is what's usually referred to as "the category of metric spaces": it seems to be more useful in practice. See eg https://en.wikipedia.org/wiki/Category_of_metric_spaces

[Edward Ayers]

Wait, wasn't this about writing a web server?

[Henry Story]

Still happy to learn about Web Programming with Lean4 :-) I guess the theme is a bit forward looking as the new Lean4 is just coming out. So the thread went all the way to looking at possibilities with HoTT.