Lean 4 as an application language

Stream: lean4

[Jesper Nordenberg]

Hi, the Lean 4 language looks amazing and it would be awesome to use as an application language (currently I use Scala and Rust, but would prefer a pure FP language with dependent types). How viable is it to use as a general application development language currently (I believe that's at least a minor goal)? I use Scala.js a lot, which is great, and I don't believe Lean 4 has a JS backend. How much effort would it be to create a JS (or WASM) backend?

[Mario Carneiro]

There have been talks about making a WASM backend, but in the short term that would probably only be compiling the generated C code to WASM

[Mario Carneiro]

which is what we already do for the in-browser version of lean

[Sebastian Ullrich]

And there's not much wrong with that, I believe

[Sebastian Ullrich]

Prior discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20and.20WASM/near/242384891

[Huỳnh Trần Khanh]

Would it be wise to make a WASM backend that directly emits WASM? I think it might be useful because if we emit WASM directly, we can emit a much smaller file.

[Huỳnh Trần Khanh]

I'm just asking. I'm not demanding anything, I swear!

[Mario Carneiro]

@Siddharth Bhat was looking into that as a possible project

[Mario Carneiro]

but also, keep in mind that if you directly emit WASM then you aren't getting any e.g. LLVM optimizations

[Sebastian Ullrich]

I'm not sure why a direct backend would generate smaller code than, say, LLVM optimizing for size; what makes you believe that? And as Mario said, you may still want some optimizations for speed. I don't know if anyone's profiled the costs and benefits of AOT optimization regarding the different WASM JITs yet.

[Jesper Nordenberg]

@Mario Carneiro Ok, that's possible of course, but maybe not the fastest turn around during development as LLVM is quite slow. With Scala.js the re-compilation is basically instant for small projects.

[Mario Carneiro]

Okay, but writing a good optimizing compiler is a tremendously huge project so it would be reasonable to expect that any homebrew solution will be much worse than an off-the-shelf compiler framework

[Mario Carneiro]

For lean, you can run things on the spot as interpreted, but the compiler takes a bit longer

[Jesper Nordenberg]

@Mario Carneiro I'm thinking more of a development build for quick iteration, and then use LLVM for final release build. This is basically what Scala.js does (but compiles to JavaScript instead)

[Jesper Nordenberg]

Mario Carneiro said:

For lean, you can run things on the spot as interpreted, but the compiler takes a bit longer

Hmm, but that doesn't work if you call from JS or use browser API's right?

[Mario Carneiro]

During development, you get live response in the editor. That's as quick iteration as you could ever ask for

[Mario Carneiro]

You can even run JS code on the spot in the widget view

[Mario Carneiro]

I don't know that much about scala.js but I don't think lean is trying to be a direct competitor

[Jesper Nordenberg]

Mario Carneiro said:

During development, you get live response in the editor. That's as quick iteration as you could ever ask for

Ok, where is this online editor?

[Jesper Nordenberg]

Mario Carneiro said:

I don't know that much about scala.js but I don't think lean is trying to be a direct competitor

It's just compiling Scala code to JS, with libraries providing access to JS API's (basically FFI). It uses the JS GC though.

[Mario Carneiro]

The editor is VSCode, which is an electron app so it integrates with a node.js backend IIUC

[Mario Carneiro]

I wouldn't recommend the online editor for serious application development

[Jesper Nordenberg]

But let's say I want to call a Lean 4 function from JS and then render stuff in a HTML canvas, then I would have to compile to WASM using LLVM?

[Mario Carneiro]

I'm saying you can literally do this in the editor, it shows up on the right side panel

[Jesper Nordenberg]

Hmm, in VS Code? Where would my canvas be rendered?

[Mario Carneiro]

It's a little outdated, but here's an example of a widget application: https://github.com/TwoFX/sudoku

[Kevin Buzzard]

Here's another one (Lean 3): https://github.com/kendfrey/rubiks-cube-group

[Jesper Nordenberg]

Oh, that's really cool! :smile:

[Jesper Nordenberg]

So, you can also add user interaction, timers etc. on the page and re-evaluate Lean functions?

[Mario Carneiro]

The whole lean document is kept up to date, it's not like python worksheets where you have to run them in order. So re-evaluation happens transparently: if you edit the code you see the changes immediately

[Mario Carneiro]

and yes, you can put user interface elements in the page to interact with the widget

[Mario Carneiro]

I think one of those puzzle game examples allowed you to click on the puzzle and it would add the corresponding move to the source code

[Jesper Nordenberg]

@Mario Carneiro Can't seem to find that. How would I call/eval a Lean function from a JS function?

[Mario Carneiro]

@Edward Ayers and @Wojciech Nawrocki are the ones to ask about Lean/JS integration

[Wojciech Nawrocki]

Jesper Nordenberg said:

Mario Carneiro Can't seem to find that. How would I call/eval a Lean function from a JS function?

Wow good timing, I am literally writing a tutorial on this now (for Lean 4) :) I can ping you when it's done.

[Jesper Nordenberg]

@Wojciech Nawrocki That would be awesome! I'm considering using it for simple game development, like updating game state based on user input and re-drawing a canvas or WebGL (similar to Elm examples).

[Wojciech Nawrocki]

Jesper Nordenberg said:

Wojciech Nawrocki That would be awesome! I'm considering using it for simple game development, like updating game state based on user input and re-drawing a canvas or WebGL (similar to Elm examples).

Then the Lean/JS interface will probably not be of much help to you, unfortunately. In this case "calling Lean from JS" means "making a remote procedure call", with JS running in a browser (or VSCode, which is a browser) and Lean running in the Lean language server. This is useful for accessing objects such as Environments and Exprs which live in the server, but not so much for general-purpose "I would rather write this function in Lean" programming. Anything low-latency has to be written in JS. As others noted above, it would also be possible to compile Lean to JS/WASM so that it can run in the client, but afaik noone has gotten that to work so far.

[Jesper Nordenberg]

@Wojciech Nawrocki Yes, I realize that. I don't care much about performance during the initial development phase (it doesn't have to be realtime). And for later release build I would definitely compile to WASM using LLVM. But maybe I'm too early adopter of Lean 4 for such an application :)

[Wojciech Nawrocki]

@Jesper Nordenberg another way to put it is that we currently have a way to invoke a remote Lean server from JS, but no way to invoke Lean code within the same execution environment that the JS is running in. So it's not just a question of performance but also ABI - to make RPC calls to remote Lean you need to encode data in various ways whereas a local call could pass it around directly. Additionally when the remote server is actually remote (i.e. on a separate machine rather than a different process on the same machine), the latency can be up in hundreds of ms which means you can really only make such calls sparingly.

[Jesper Nordenberg]

@Wojciech Nawrocki Ok, I suppose the only viable way is to compile to WASM then for testing

[Reinier van der Gronden]

@Wojciech Nawrocki is your method of calling a Lean function from JS different from the User Widgets? I'm investigating this right now because I want to talk between Lean code and infoview for code improvement suggestions, but it seems that one of your latests point on having to encode all data to the Lean server complicates the use of TacticM, because all MVars and contexts are likely difficult to communicate, currently widgets seem to build on top of TermElabM.

[Wojciech Nawrocki]

@Reinier van der Gronden no, it is exactly the method described there. Here is an example of how we can send a tactic context to and from the infoview. I suppose we should also have a section about this in the User Widgets tutorial.

[Reinier van der Gronden]

@Wojciech Nawrocki Thanks for that pointer, I'll take a look!