UI in Lean

Stream: new members

[Dan Abramov]

Has anyone attempted to write some kind of UI library/framework in Lean? I mean something React-like but actually written in Lean. Does the question even make sense? I guess maybe not without JS bindings. But maybe there are some DOM-like native targets that this could be prototyped against? I'm mostly just interested in the ergonomics of writing React-like components in Lean so I don't actually care what the underlying target is.

[Kyle Miller]

There's https://github.com/leanprover-community/ProofWidgets4 for writing UI in Lean. You get to use a DOM, and it uses React. Widgets show up in the Infoview.

Somehow there's some RPC interface between Lean and Javascript for this for interactive widgets. I think it's sort of a server-client model, with Lean and Javascript-with-DOM.

[Dan Abramov]

Interesting. This is fun but I guess I mean pure Lean, in the sense that the component model itself and reconciliation happens in Lean. My interest isn't anything practical but more like what a pure implementation of React reconciliation would look like.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

reconciliation happens in Lean

The original implementation of ProofWidgets in Lean 3 did this; have a look at @Edward Ayers PhD thesis. In that setting, reconciliation happens in the Lean server. This can unfortunately result in quite unresponsive UI when the JS client in which widgets appear and the Lean server are on different physical machines. So in the Lean 4 version, we made the decision to run widget code (including reconciliation) in clients using vanilla React; I would still like to see a Lean API for writing these, but that seems to basically require a Lean-to-JS compilation target. I don't know of anyone working on that atm.

(Also here are some prior discussions of Lean-WASM.)

[Rado Kirov]

Not directly related (sounds like there isn't any Lean UI library at the moment), but given Lean's Haskell adjacency, https://www.altocumulus.org/Fudgets might be of interest. It's ancient, unmaintained, no idea if any serious UI was ever built with it, but if one rebuilds a UI libary in Lean it might end up looking similar (due to purity, focus on composition and algebraic thinking).

[Mr Proof]

What would be the use case? If you want to interface with Lean from a UI perspective. It may be simpler to write something in a standard language like C# or python or javascript and interface with the Lean kernel.

If you wanted just a dependently typed programming language for making general apps, then Idris would probably be a better choice.

It would be nice if Lean became a general purpose programming language for making apps but I don't think it's going that way...

[Rado Kirov]

making general apps, then Idris would probably be a better choice.

OOC, what are the differences - core language, or existing ecosystem or something else?

[(deleted)]

I think it's just an opinion.

[(deleted)]

I don't agree with it.

[Artur Lojewski]

Dan Abramov said:

Has anyone attempted to write some kind of UI library/framework in Lean? I mean something React-like but actually written in Lean. Does the question even make sense? I guess maybe not without JS bindings. But maybe there are some DOM-like native targets that this could be prototyped against? I'm mostly just interested in the ergonomics of writing React-like components in Lean so I don't actually care what the underlying target is.

What I like to see is whether lean4 (since it is a functional language) could re-implement (?) something like....

https://elm-lang.org
https://elm-lang.org/try

Elm is a functional programming language that compiles to JavaScript, and is used for websites and web apps. I find it vy user friendly! Would love to see that! :slight_smile:

[Kyle Miller]

@Mr Proof Just to clarify, the Lean kernel is only one element of the Lean system, and it's not what you'd interface with for general-purpose programming. Lean is a general-purpose programming language, and that is one of the project's primary goals. Most of Lean is written in Lean, even the LSP server and compiler, and it compiles to efficient code. You would interface with compiled Lean code, which uses a C ABI.

You can use that C ABI to bind to existing GUI libraries. Idris does not appear to have native GUI libraries either, so it's unclear what the advantage is.

[Kyle Miller]

@Artur Lojewski I'm looking forward to one day someone making a JS or WASM backend. There are some things I've written in Javascript that I'd love to be able to rewrite in Lean and feel more confident in being correct!

That's not exactly what you're suggesting, but if there were such a backend, with Lean's powerful metaprogramming features I don't see why there couldn't be some Elm-like DSL in Lean.

[Mr Proof]

Well, it's just my opinion. The lean roadmap doesn't seem to prioritise making it a user interface based langauge.

If I wanted to write a Tetris game for a mobile phone, Lean would be the last language on my list to use. But I'm prepared to be proved wrong.

It shouldn't be too hard anyway to support windows API calls within Lean. If you can call functions from a DLL that's basically all you need. But, I don't know why that would be better?

BTW last year I tried to make a UI in C# to run Lean, but when I found the MathLib library took up about 4GB of RAM to run I gave up. But I think there's been improvements since then e.g. incremental loading.

[Rob Simmons]

@Dan Abramov I was immediately interested in this family of questions as well, both because of my experience with Elm and because of working on the more restricted "diagrammar" widget toolkit at Brilliant (strangeloop talk about that).

The leansplat-demo.mov here is a VERY hacked together tech demo I made that was actually using Lean metaprogramming to coax expressions in Lean's kernel language into javascript on the filesystem, and then using Vite to pick up those filesystem changes and refresh the page.
leansplat-demo.mov

[Rob Simmons]

Based on subsequent conversations I think you wouldn't want to actually hook into metaprogramming where I was choosing to do so, but I think trying to build an Elm Architecture-style setup this way could be quite cool.

[Rob Simmons]

maybe this'll embed better:

ezgif-2efc21f7c7c1f0.gif