LeanToDo: creating a web app using Lean

Stream: general

[pandaman]

I'm happy to share an experiment in building a web application with Lean:

https://leantodo.fly.dev/

It’s a simple in-browser todo app for creating and managing todos. This project uses two excellent Lean libraries by @David Thrane Christiansen:

• leansqlite for database
• Verso for HTML templating

I see a lot of potential in Verso's HTML output for web development. It provides a JSX-like experience and makes it easy to compose HTML components in Lean using data pulled from SQLite. It also pairs nicely with HTML-centric tools like HTMX and Tailwind CSS.
I could even enable the Tailwind VSCode extension to auto-complete utility classes inside Verso's HTML macros!

This repository has no proofs or dependent types. It's mostly procedural code and side effects. I hope it’s another useful example that Lean can be used for “normal” software, including web applications.

The code is available at https://github.com/pandaman64/LeanToDo. Thank you!

[David Thrane Christiansen]

I'm glad you had a good experience! How did you like the interpolation API for SQLite prepared statements?

[Kim Morrison]

@pandaman, this is awesome! Lovely to see all these new ecosystem capabilities in action.

If you really want to live on the bleeding edge, Lean is getting its own HTTP server which you could use, see lean#12151. (Or just set your lean-toolchain to leanprover/lean4-pr-releases:pr-release-12151, yolo...)

[pandaman]

The query! macro was nice. Things like implementing SQLite.Row and handling Stmt felt a bit low level, but I can definitely see a future where these are nicely wrapped.
I'll definitely try Lean.HTTP as I want to get rid of GPT's hacky implementation:joy:

[David Thrane Christiansen]

If you have suggestions for how to make the API more convenient, I'm all ears. This is the early days of it, and improvement driven by real use are very welcome. Or would deriving SQLite.Row have been sufficient?

[David Thrane Christiansen]

There's now a deriving handler for Row, along with QueryParam and ResultColumn.

[Patrick Massot]

I’m very curious about the motivation for this sql stuff. David is there any information you’re allowed to share about why you worked on that?

[David Thrane Christiansen]

I'm in the process of redoing how Verso gets docstrings when rendering the manual. Right now, it looks in the environment, but this won't work with the module system because docstrings are stored in the server olean and aren't loaded in command-line builds. So instead doc-gen will be set up to dump a database in addition to HTML, and Verso will get them from the database.

[David Thrane Christiansen]

SQLite isn't strictly necessary for this, but it makes many things easier. Cross-cutting queries like "give me all the instances for this type" can run efficiently without needing to put work into how we represent the dumped data, and this flexibility will make it feasible to make Verso's output richer as well.

[David Thrane Christiansen]

It's also much easier to debug - there's great tools for SQLite already

[David Thrane Christiansen]

Being able to use the module system in the manual will greatly reduce incremental build times. The idea is to have the turnaround from "changed text in chapter 5" to reading the text on the screen be as short as possible.

[Patrick Massot]

Great!

[Nilesh]

@David Thrane Christiansen Something that might be a lot of fun to explore for SELECT queries is to model them as composable data pipelines. https://prql-lang.org/ calls this "orthogonality of transformations".

[David Thrane Christiansen]

Right now my goals are more aligned with getting tools out the door than exploration, but I'd love to see what you can come up with should you decide to explore it!

[pandaman]

If you have suggestions for how to make the API more convenient, I'm all ears. This is the early days of it, and improvement driven by real use are very welcome. Or would deriving SQLite.Row have been sufficient?

The deriving handlers are great, but in general, I don't have a good answer.

I'd expect there will be several "opinionated" approaches, including:

• Type and code generation a la sqlc
• type-safe query builder a la diesel
• Or we could even bring SML#'s SQL feature to Lean, having a type system capable inferring SQL types!

I don't see the programming community is converging on a single solution, and I'd love to see experiments around this area in Lean on top of lower-level bindings for SQLite, Postgres, MySQL, etc. (If I had infinite time...)

[David Thrane Christiansen]

Those sounds good!

I wanted to avoid spending a bunch of time innovating on the interface to SQLite here, and focus on providing fairly complete bindings at a lower level, plus a certain minimum of convenience features like the result set iterator. I hope this library can be a basis for higher-level ones like you're describing, but those kinds of features are outside my current scope.

Let me know if other papercuts come up, at least.

[pandaman]

Yeah, I think people can build their favorite high-level frameworks on top of bindings like yours.

Let me know if other papercuts come up, at least.

Will do. And thank again for the great library!

[David Thrane Christiansen]

Thanks for the good feedback, and for using it!

[Nicolas Grislain]

Nice!
If you want to use PostgreSQL for your backend, you may check these:

• github.com/typednotes/lean-pq (I wrote it, it's a binding to libpq)
• github.com/kaito2/lean-pq (looks cool, it's a rewrite of the postgres protocol in pure lean)