First release of "Functional Programming in Lean"

Stream: lean4

[David Thrane Christiansen]

This is a re-post from #announce, because that's not a great place for follow-up discussion.

With generous support from Microsoft Research, I've been working on an online book called _Functional Programming in Lean_. The goal of the book is to be an accessible introduction to using Lean 4 as a programming language. My hope is that it is useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming. I'm not assuming any background with FP, though it's probably not a good first book on programming in general.

New content will be added once per month until it's done. I'll announce new updates here and in the usual venues.

You can read what's there and follow along with the development at https://leanprover.github.io/functional_programming_in_lean/ .

I'd like this book to be as useful as possible, and feedback is always welcome if there's some part that you didn't understand. You can contact me here or at david@davidchristiansen.dk.

[Patrick Massot]

This is really nice. It will be really useful in combination with the metaprogramming book that basically assumes people have read this one.

[Patrick Massot]

Do you have any idea how soon you'll have covered enough monad magic to read that metabook?

[Henrik Böving]

As an idea for David what counts as "enough monad magic", the metaprogramming book takes over at monad transformers and stacks, everything up to that is assumed as given.

[Patrick Massot]

Henrik, are you sure the latest version covers transformers and stacks? I think that got removed

[Henrik Böving]

It's in the temp/ folder right now but not rendered yes.

[Henrik Böving]

https://github.com/arthurpaulino/lean4-metaprogramming-book/tree/master/temp here

[Henrik Böving]

Though it would make sense to eventually move this knowledge to functional programming in lean I think.

[Patrick Massot]

I'm an old man, I printed the book two days ago. Nothing else exists :stuck_out_tongue_wink:

[David Thrane Christiansen]

There'll likely be a few months until then. I expect the next few chapters to have this rough outline:

• "Hello world", including how to think about side effects in a pure language, though without the M-word, along with practical tasks like how to use the compiler to build executables
• Type classes as a principled way to do ad-hoc polymorphism
• Monads for things like Option
• Revisit "hello world", show how do-notation works, cover the nifty Lean features
• Do other stuff for a while...
• Then do some monad transformers and introduce big parts of the Lean library that use them

[Henrik Böving]

Patrick Massot said:

I'm an old man, I printed the book two days ago. Nothing else exists :stuck_out_tongue_wink:

You actually went through with it hahaha.

[Henrik Böving]

David Thrane Christiansen said:

There'll likely be a few months until then. I expect the next few chapters to have this rough outline:

• "Hello world", including how to think about side effects in a pure language, though without the M-word, along with practical tasks like how to use the compiler to build executables
• Type classes as a principled way to do ad-hoc polymorphism
• Monads for things like Option
• Revisit "hello world", show how do-notation works, cover the nifty Lean features
• Do other stuff for a while...
• Then do some monad transformers and introduce big parts of the Lean library that use them

I think one of the reasons patrick is asking is that towards the end of july there is a plan to teach a bunch of Lean mathematicians how to meta program in lean 4 so they can help porting the tactics over and for that it would be optimal if we had resources that lead the way from very little Lean 4 programming knowledge to meta programming.

[David Thrane Christiansen]

I'm working as fast as I can on this, but I'm not so sure that I can get all the way to monad transformers by July. But let's check in at the next release and see where things stand.

[Patrick Massot]

Indeed that's part of the motivation. It seems that Lean 4 requires more monadic understanding than Lean 3.

[Patrick Massot]

In Lean 3 I was able to write https://leanprover-community.github.io/extras/tactic_writing.html which covers very little monadology and still allows to write easy tactics.

[Julian Berman]

Not sure how important it is at this very moment but have you given any thought to contacting a publisher? O'Reilly at least always says they're trying to find the next new thing. Maybe they'd be interested in funding some of the writing of these books (which yeah seems also super helpful!).

[Julian Berman]

Ah sorry, I see you said you're already getting supported by MS.

[Adam Topaz]

Patrick I'm curious why you say that Lean4 requires more monadic understanding? Is it because of the uses of lifts all over the place? I would think the fact that you can write for loops in the usual way is an argument against this claim!

[Patrick Massot]

Yes, I'm thinking about liftWhatever and withStuff that appear everywhere. The words "monad stack" and "monad transformer" don't appear anywhere in our elementary Lean 3 tactic writing documentation (and I don't think they appear in Rob's lectures).

[Patrick Massot]

However this is a very superficial comment. I only claim I see things that I didn't need to know in Lean 3 and seem really important from the very beginning here.

[Kevin Buzzard]

I spoke in ETH Zurich last Friday and after the talk a Springer/Birkhäuser publisher approached me and asked if I was interested in writing a book. I said no but I can pass their details on if you're interested.

[Arthur Paulino]

I think tactic writing / monadic programming in Lean 4 can look scarier because the syntax is richer, there are more monads and the API is more extensive. But in the very core, it's still monads and the fundamental concepts remain

[Siddhartha Gadgil]

In my personal experience one can work with liftWhatever and withStuff without really knowing monad transformers. Signatures of these things and examples (from the lean 4 source, now from the metaprogramming book) are often enough.

[David Thrane Christiansen]

The book is for free on the Lean web page - no publisher needed right now, but that might be a nice way to extend the reach of Lean someday. I was also very happy with my experience with the MIT Press for _The Little Typer_, so they'd be good to talk to.