new lean4-samples repo

Stream: lean4

[Chris Lovett]

We have a new github repo for lean4-samples so if any one has any ideas for some great samples please list your ideas here, or feel free to submit a PR. The VS Code lean4 extension will be highlighting some of these samples in the Lean4: Open Documentation View.

[Henrik Böving]

What qualifies as a great sample? Should it be particularly simple to digest?

[Chris Lovett]

Good question, love to know what everyone thinks for Lean, but I'm sure it will evolve over time. I like samples that do something fun, that can be organized into a meaningful taxonomy over time, are not too huge (upper limit in the thousands of lines of code) and have good documentation on how they work both in readme and code comments. They also show best practices, and useful programming patterns. I think it's best if readers can "grock" most of the sample code in a couple hours max.

[Julian Berman]

Maybe a good sample is "how do I write a FFI-using wrapper for a C library"? I stole a thing or two from @Arthur Paulino's MySQL repo to try to do so but it may be a useful pattern to show more generally. (I think this kind of repo is a perfect idea)

[Chris Lovett]

Would be super cool if we could create a MySQL (or better yet SQLite) wrapper that implements LINQ to SQL-style embedded DSL's in Lean!! That would be a convincing proof of the usefulness and power of Lean4 extensibility. And would be useful for implementing Lean package manager local cache indexes...

[Yuri de Wit]

Another cool thing, that probably could be useful for LINQ-to-SQL too, is Type Providers: https://docs.microsoft.com/en-us/dotnet/fsharp/tutorials/type-providers/

[Chris Lovett]

@Yuri de Wit perfect, that's what I was imaging also when I said this

[Joseph O]

I think a small interpreter written in lean would be a great example. Possibly a small lisp, or a more complicated example using combinators, though that would be less beginner friendly