Guide for OOP devs?

Stream: new members

[James B Clifford]

Hi All. Any guides for non-functional developers? I'm trying to learn lean4 and having a bit of a time with it. I've mainly worked with OOP in the past. I have serval questions about making the transition to lean. I'm getting a real "just go read the source vibe" (e.g. https://leanprover.github.io/lean4/doc/list.html is blank) is there any docs that i'm missing?

[Henrik Böving]

There is a WIP programming book: https://leanprover.github.io/functional_programming_in_lean/
There is docs: https://leanprover-community.github.io/mathlib4_docs/
There is TIPL4: https://leanprover.github.io/theorem_proving_in_lean4/

And there is indeed the source code^^ And also the lean4 topic if you have further questions.

[Eric Wieser]

(#lean4 is a "stream" not a "topic")

[James B Clifford]

I've read through https://leanprover.github.io/theorem_proving_in_lean4/ which was very math heavy for me. I received a MS in compsci in 2018, but I haven't done any proofs since discrete math in undergrad around 2002.

I started https://leanprover.github.io/functional_programming_in_lean/ but that feels like it expects that you already know functional programming and is teaching you the syntax of lean for the concepts you already know. Haskell is mentioned a few times in there, should I go learn that first?

I really am interested in learning this language as programming language (i.e. to produce executables), I'm just having a bit of trouble getting started.

[Arien Malec]

You could read Learn You a Haskell for Great Good! then do all the same exercises in Lean….

[Jason Rute]

Here is a stack exchange answer I wrote which might help you a bit: https://proofassistants.stackexchange.com/questions/1701/a-project-in-lean-which-involves-programming/1708#1708

[Jason Rute]

Even more tenuous, but here are some notes I made on functional programming for people who only know Python, but honestly you might be better off with a more standard piece of documentation: https://github.com/jasonrute/functional_programing_workshop

[Jason Rute]

in general don’t be discorouaged. Functional programming is a different way to think about code and will take a little time to learn.

[James B Clifford]

@Jason Rute your https://github.com/jasonrute/functional_programing_workshop guide is actually very helpful. Thank you. Comparing it to the declarative nature of SQL helps a lot. I have a question is how would you go about translating a simple class with properties and methods into a functional language?

[James B Clifford]

@Arien Malec this one? http://learnyouahaskell.com/chapters

[Arien Malec]

That’s the one…

[Jason Rute]

@James B Clifford I would caution against trying to cram an object oriented approach into Lean code, but here is some advice. Structures in Lean are the closest thing to classes in the sense of that they store fields of multiple information (and you can use the usual dot notation to access a field). Inductive types are similar and more general, but use a more functional notation. They are needed if you want your type to be recursive. As for class methods, usually all you are interested in is having functions associated with a particular type. In lean z.abs is the same thing as Int.abs z. The idea is just that if a function is under the Intnamespace, then you can use dot notation and the thing to the left of the dot is put in for the first argument of that type.

[James B Clifford]

@Jason Rute kinda reminds me of the old GTK+ style of "classes" in ANSI C. where, for example a linked list, would declare a struct linked_list and a set of functions with declarations like linked_list_blank(struct linked_list *self, ...). but you are right, I should stop thinking in classes.

[Julian Berman]

Arguably OOP doesn't have much to do with classes either!

[Arien Malec]

I think that's right -- "pragmatic" languages built on HM type theory, like Swift, are used by "regular old developers" who don't read Category Theory for the Working Programmer, and mostly they model stuff with structs (spelled structure in Lean) and enums (spelled inductive in Lean).

These days many modern "OO" programming languages have Hindley-Milner type systems bolted on, and heavily use functional programming around containers. And while typeclasses can do crazy impressive things, they also play the same role that Java/C# interfaces do.

Where you want a bag of properties, use a structure; where you want to model something like a state machine or flags, use an inductive, where you want to model what you might have done in an abstract class or an interface, use a class.

When you want to model OO design patterns, learn what a monoid in the category of endofunctors is...

[Patrick Massot]

James B Clifford said:

I started https://leanprover.github.io/functional_programming_in_lean/ but that feels like it expects that you already know functional programming and is teaching you the syntax of lean for the concepts you already know. Haskell is mentioned a few times in there, should I go learn that first?

I think you should rather talk with the author @David Thrane Christiansen. This book isn't meant to assume you know functional programming. Anyone saying "you should first read Learn you a Haksell first" should talk to David to understand why they think this.

[Patrick Massot]

And of course thinking in terms of "how can I write python in Lean?" is a very bad starting point to learn Lean, and the same is true with any pair of distinct programming languages instead of (python, Lean), although it is very tempting in the beginning.

[Jason Rute]

I was recently looking at the tutorial for Isabelle (as a theorem prover) and I was shocked to see that it explicitly said you should know some functional programming first. That really puts up a barrier to entry. I really appreciate that TPIL and FPIL at least try to be a self contained intros with little or no background.

[Jason Rute]

Also one more piece of advice that hasn’t been said is to just to pick small programming tasks and just start to code them in Lean. (Some like Advent of Code.). This is how I learned Python. I find having a practical, but simple task is a great way to get past the abstract barrier and figure out how to actually accomplish stuff in a particular language.

[Yaël Dillies]

Let me mention that @Bhavik Mehta stumbled upon that message when learning Isabelle (or was it another ITP?), so he went onto learning Haskell, and proceeded to forget about Isabelle :stuck_out_tongue_closed_eyes:

[Bhavik Mehta]

Agda rather than Isabelle - the first tutorial I found at the time said "learn Haskell first"

[Bhavik Mehta]

It was this: http://learnyouanagda.liamoc.net/pages/introduction.html

[Pedro Sánchez Terraf]

Jason Rute said:

I was recently looking at the tutorial for Isabelle (as a theorem prover) and I was shocked to see that it explicitly said you should know some functional programming first. That really puts up a barrier to entry.

I'm a user of Isabelle, and though I like it very much, we really struggled to get started. It seems that your are meant to subscribe to the mailing list and ask everything there. Now Paulson started a blog, with some entries that might serve as a better introduction.

[Arien Malec]

Just going through FPIL, it starts in pretty deep water in the prelude, but then goes back to basics but dives back into deeper waters from time to time, often when explaining why you might get certain errors….

[Arien Malec]

& of course certain basic questions (how do I read a file) have a tendency to get complicated all by themselves.

[Arien Malec]

Tho FPIL does a good job of not using the “M” word.

[David Thrane Christiansen]

Arien Malec said:

Tho FPIL does a good job of not using the “M” word.

Beware! The chapter on the M-word is coming out Very Soon!

[David Thrane Christiansen]

James B Clifford said:

I started https://leanprover.github.io/functional_programming_in_lean/ but that feels like it expects that you already know functional programming and is teaching you the syntax of lean for the concepts you already know. Haskell is mentioned a few times in there, should I go learn that first?

My intention with the book is that you should not need to know any functional language to use it, and I have tried hard to ensure that each step is explained and documented in the book itself. Any references to Haskell or ML are there to give proper credit to the origins of important ideas. That said, nobody's perfect, and I'm sure there are spots in the book that take steps that are too long. It would be very useful for me to know where the book lost you so that I can make it better! I hope that you will let me know.

[Arien Malec]

Just came across this & it’s quite good

[Arien Malec]

https://agentultra.github.io/lean-4-hackers/

[James B Clifford]

https://vimeo.com/113588389
This F# video was very helpful

[Tyler Josephson ⚛️]

I appreciate this intro to functional programming: https://youtu.be/0if71HOyVjY

[Arthur Paulino]

Before getting into Lean, my only previous experience was with imperative languages. ~18 years of C, C++, Java, Python and Javascript mostly. And of course I struggled a lot with Lean. In my experience, trying to mimic my previous ways of thinking about computation just slowed me down. So I just opened myself up to new mindblowing experiences, similar to the first ones I had when I was learning about programming for the first time. I was used to thinking like a turing machine and then I had to start thinking more like lambda calculus