Lean 4 as a general programming language

Stream: general

[Jesper Nordenberg]

Hello, I'm new to Lean and I find it a very interesting project. My question is if Lean 4 is meant to be able to be used as a general application programming language in the same sense as Rust, Haskell, Scala, Idris etc? Will you be able to write efficient desktop/server/JavaScript applications in Lean?

If so, is there (planned) support for C-like primitives like unboxed fixed sized primitive types, structs and arrays? I suppose so since there seem to be a foreign C function interface and there are many compiler optimization for memory handling etc.

[Kevin Lacker]

Basically no, it may be possible to write a general application in Lean 4 but it will not really be a good idea. Things you need for general programming like encryption or networking libraries are extremely low priority or perhaps never-to-be-implemented for lean

[Jesper Nordenberg]

Can those not be provided using FFI calls? Though t
hat probably requires that the Lean compiler has support for C-like primitives the same way Rust (and Haskell to a certain extent) has for example

[Kevin Lacker]

I just think you will have a miserable time doing it. It might technically be possible. It's like writing an ssh client in redstone in minecraft, sure it's probably possible in theory, but it's really not what the tool is designed for

[Marc Huisinga]

Kevin Lacker said:

I just think you will have a miserable time doing it. It might technically be possible. It's like writing an ssh client in redstone in minecraft, sure it's probably possible in theory, but it's really not what the tool is designed for

i mean, lean 4 is implemented in lean 4. i don't see why using lean 4 as a general purpose programming language is so outlandish.

[Marc Huisinga]

for libraries you can use the FFI, yup.

[Kevin Buzzard]

My impression was that Leo wanted Lean 4 to compete with Haskell, but I don't know what they are competing over, perhaps the scope is less broad. Someone on the Discord made a Sudoku game in Lean 3 :-)

[Jesper Nordenberg]

I just read the paper about the RC implementation in Lean 4 and it definitely seems to be generally applicable to general functional programming languages (I believe it even says so in the paper), but maybe the optimizations in there were primarily to make theorem proving faster.

[Marc Huisinga]

the majority of programming primitives in lean 4 already have an efficient C backend. e.g. arrays or integers.

[Jesper Nordenberg]

Marc Huisinga said:

the majority of programming primitives in lean 4 already have an efficient C backend. e.g. arrays or integers.

Is there support for 32- and 64-bit fixed width integers for example? And "flat" arrays?

[Kevin Lacker]

let me put it this way... if you are looking to write "efficient desktop/server/JavaScript applications in Lean", then you should first think of the libraries that such applications would need. in particular, you'll need an HTTP library and some way to deal with the system's UI. you either have to write those yourself, or someone has already made some for Lean. writing those yourself is probably a bad idea, or at least it will take a while.

[Kevin Lacker]

maybe someday those things will exist in Lean. Lean 4 is certainly progress in that direction. however, this set of features isn't on the horizon, so, i wouldn't hold my breath

[Alex J. Best]

You might enjoy @Sebastian Ullrich's demo as part of Lean 4 @ PLDI 2020 if you haven't seen it
https://www.youtube.com/watch?v=TgHISG-81wM (47:41 in), and of course the talk itself is very informative about what the developers want lean 4 to be.

[Marc Huisinga]

Jesper Nordenberg said:

Marc Huisinga said:

the majority of programming primitives in lean 4 already have an efficient C backend. e.g. arrays or integers.

Is there support for 32- and 64-bit fixed width integers for example? And "flat" arrays?

i'm not sure if fixed-width integers in particular exist yet, but there are uint* types: https://github.com/leanprover/lean4/blob/master/src/Init/Data/UInt.lean

[Jesper Nordenberg]

@Kevin Lacker Depends, if you for example have a JavaScript backend you can quite easily write web application with some FFI to the browser API's

And a basic web server doesn't require that many system libraries

[Jesper Nordenberg]

@Marc Huisinga Interesting, ByteArray and FloatArray seem to be available as well

[Jesper Nordenberg]

@Alex J. Best Yes, I watched that video, very informative

[Kevin Lacker]

I guess it depends on the application you're thinking of... why would you want to use lean for a web application? if you wanted to do something like, a user enters some mathematical formula, and lean tries to prove it, then it might make sense. but you'd probably be better off making the bulk of the web app in something else, and keeping the lean process separate. easier to just interact between the processes in one spot rather than FFIing a bunch of stuff with a web server

[Jesper Nordenberg]

@Kevin Lacker Well, I want to use a powerful functional programming language to write efficient applications with. There's not a lot of choices available, Scala is nice but not as powerful as Lean and Idris (at least in some ways), Rust is very efficient but also low level and quite restricted, Haskell is tricky to write efficient code in etc.

[Jesper Nordenberg]

To me it seems like Lean has the potential to be both very powerful and efficient considering the memory management optimizations and FFI possibilities

[Marc Huisinga]

Kevin Lacker said:

why would you want to use lean for a web application?

perhaps because you like it as a functional language :)
in my experience, disregarding the fact that we don't have a language server with all the bells and whistles yet, lean 4 is already quite nice to use as a functional programming language.
not all of the cool stuff is documented yet, but there's some stuff: https://leanprover.github.io/lean4/doc

[Marc Huisinga]

(i think lean 4 being a good functional programming language is also very good for theorem proving :))

[Jason Rute]

I’m curious what you mean by Scala is not powerful enough. I don’t mean to get into a flame war, but I think more production applications are written in Scala than most other functional programming languages. Maybe by power you mean something about functional/type-theoretic power?

[Jason Rute]

I’m referring to @Jesper Nordenberg‘s comment above.

[Jesper Nordenberg]

@Jason Rute Scala 3 is definitely more powerful than most common languages and I like it a lot, but it's not a dependently typed pure functional language like Idris and Lean. It's also not as runtime efficient as for example Rust (there are no unboxed structs and arrays, dependent on GC etc.).

[Jesper Nordenberg]

It seems Lean has @[specialize] and @[inline] annotations, are those similar to what's found in Rust?

[Marc Huisinga]

this is best answered by @Sebastian Ullrich when he's online :sweat_smile:

[Jesper Nordenberg]

Ok, I will try to have a chat with him, thanks!

[Jason Rute]

By the way, since we are talking about Lean as a fast to execute language, will tail recursion be optimized in Lean 4?

[Mario Carneiro]

isn't that a requirement? After all there are no for loops

[Mario Carneiro]

Here is evidence that the interpreter does tail recursion. However this is the "slow path", in practice we care more about the performance of lean 4 code after it's been compiled to LLVM, and my understanding is that tail recursion is not guaranteed by LLVM.

[Marc Huisinga]

Mario Carneiro said:

After all there are no for loops

well, in some sense ... https://leanprover.github.io/lean4/doc/do.html#iteration :grinning:

[Mario Carneiro]

well it's still a DSL, it gets elaborated into maps and folds

[Jesper Nordenberg]

Jason Rute said:

By the way, since we are talking about Lean as a fast to execute language, will tail recursion be optimized in Lean 4?

Yes, they mention "join points" in their paper. They are never partially applied and calls are translated to a simple jump instructtion.

[Sebastian Ullrich]

@Kevin Lacker I'd appreciate it if you didn't assert the goals of a project you're not involved in. The first paragraph of https://leanprover.github.io/lean4/doc/ plainly states what Lean 4 is intended to be: both a general-purpose programming language and an interactive theorem prover. Of course there's no web server when the language hasn't even seen its first release yet! It's true that those things are not exactly on our to-do list, but they are not part of the stdlib in many other languages (Haskell, Rust, ...) but have been implemented by third parties instead.

FWIW, I have high hopes for exploring integration with Rust's vast ecosystem. Rust is quite similar to Lean 4 in a few regards that make integration more feasible: safe, high-level and functional-ish APIs (no OOP, avoids mutable aliasing), yet no tracing GC. And thanks to reference counting, we can at least check for linearity at run time if not statically. Not sure when I'll get to working on that though... :) .

[Sebastian Ullrich]

Jesper Nordenberg said:

If so, is there (planned) support for C-like primitives like unboxed fixed sized primitive types, structs and arrays? I suppose so since there seem to be a foreign C function interface and there are many compiler optimization for memory handling etc.

Unboxed primitive types and arrays of those has already been mentioned here, but there is no support for unboxed product types yet.

[Sebastian Ullrich]

Jesper Nordenberg said:

It seems Lean has @[specialize] and @[inline] annotations, are those similar to what's found in Rust?

Our inlining is comparable to that in any other optimized language, I suppose. Specialization is more of a hint like in Haskell than the pervasive, obligatory specialization automatically done in Rust, which they need to support zero-cost passing of unboxed types.

[Sebastian Ullrich]

Jesper Nordenberg said:

Jason Rute said:

By the way, since we are talking about Lean as a fast to execute language, will tail recursion be optimized in Lean 4?

Yes, they mention "join points" in their paper. They are never partially applied and calls are translated to a simple jump instructtion.

Our join points are not recursive, but the C backend eliminates direct tail recursion instead. It's definitely feasible to implement more general TCO, but there was no need so far.

[Jesper Nordenberg]

Thanks for the info, really interesting project.

[Jesper Nordenberg]

Sebastian Ullrich said:

FWIW, I have high hopes for exploring integration with Rust's vast ecosystem. Rust is quite similar to Lean 4 in a few regards that make integration more feasible: safe, high-level and functional-ish APIs (no OOP, avoids mutable aliasing), yet no tracing GC. And thanks to reference counting, we can at least check for linearity at run time if not statically. Not sure when I'll get to working on that though... :) .

Oh, do you plan to be able to call Rust functions and use Rust types directly in Lean? That sounds pretty awesome. :smile:

[Jesper Nordenberg]

Sebastian Ullrich said:

Our inlining is comparable to that in any other optimized language, I suppose. Specialization is more of a hint like in Haskell than the pervasive, obligatory specialization automatically done in Rust, which they need to support zero-cost passing of unboxed types.

Is there some heuristic in the compiler for when to apply specialization? I think specialization is crucial to get the same level of performance for abstractions as in Rust and C++.

[Jesper Nordenberg]

Btw, Swift has a really interesting approach to monomorphization and specialization that avoid the code bloat of C++ and Rust

[Sebastian Ullrich]

You mean dictionary passing with size information? I would rather call that avoidance of specialization :) . And it will only become relevant when we have unboxed types above the pointer size.

[Sebastian Ullrich]

Jesper Nordenberg said:

Oh, do you plan to be able to call Rust functions and use Rust types directly in Lean? That sounds pretty awesome. :smile:

We have to do something with our arbitrary code-executing macros after all! Such as calling foreign compilers on the fly...

[Sebastian Ullrich]

Jesper Nordenberg said:

Is there some heuristic in the compiler for when to apply specialization? I think specialization is crucial to get the same level of performance for abstractions as in Rust and C++.

Some heuristics are necessary to avoid unnecessary specialization of e.g. Nat parameters. But this is part of the C++ part of the compiler that will be rewritten in Lean anyway, so it might change during that.

[Jesper Nordenberg]

Sebastian Ullrich said:

You mean dictionary passing with size information? I would rather call that avoidance of specialization :) . And it will only become relevant when we have unboxed types above the pointer size.

Yes, that's what mean. They can avoid boxing without doing monomorphization.

[Kevin Lacker]

@Sebastian Ullrich I certainly wish you luck in making lean 4 a good general programming language! I would be interested in helping out, for example while using Lean 3 I have often wanted libraries that exist in other programming languages, like different data structures. I hope there is eventually some process for the community to contribute to Lean 4.

[Joe Hendrix]

I've been using Lean 4 for a while as a programming language. It's not "general purpose" since we are building a verification tool, but as part of that we have an x86 semantics, bindings to LLVM, SMTLIB generation, and an Elf parsing library.
I don't really see any reason you can't use Lean 4 as a general purpose language if you want to build native binaries (as opposed to webapps, etc). It's also relatively easy to write bindings to C libraries. The language is still in development, and I'd still recommend the vast majority of people use Lean 3 or a more mature language for now.
Performance has generally been quite good. I sometimes have to be careful about inadvertently blowing up the stack in code that would be fine in Haskell, but that can be fixed by refactoring. The compiled code is generally quite efficient otherwise.
I think the community will develop when Lean 4 is released; I haven't yet used this myself, but it certainly seems like the metaprogramming facilities will allow the community to extend Lean in many different ways without needing to contribute to the Lean 4 core.

[Mario Carneiro]

Oh, I had no idea the galois code was public

[Joe Hendrix]

@Mario Carneiro I don't think it's actually useful to others, but it's all currently public. :)

[Wrenna Robson]

I was just saying to @Kevin Buzzard elsewhere that I couldn't believe my interests were intersecting.

[Wrenna Robson]

Having spent half this year learning Cryptol, here's someone from Galois!

[Alexandre Rademaker]

How can we test lean 4 without breaking the current installation ? Elan can manage both versions, right ?

[Jason Rute]

There are installation instructions here: https://leanprover.github.io/lean4/doc/make/index.html. You have to compile from the source. (It also gives some elan linking instructions, but I have just been running it directly from the command line using the full path to the binary. But that means I’m not using any language server support.). For my setup at least, there is no issue with having both installed.