Zulip Chat Archive

Stream: new members

Topic: Guide for OOP devs?


James B Clifford (Nov 23 2022 at 22:54):

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 (Nov 23 2022 at 23:11):

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 (Nov 24 2022 at 00:36):

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

James B Clifford (Nov 24 2022 at 00:57):

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 (Nov 24 2022 at 01:09):

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

Jason Rute (Nov 24 2022 at 01:15):

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 (Nov 24 2022 at 01:19):

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 (Nov 24 2022 at 01:20):

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 (Nov 24 2022 at 01:40):

@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 (Nov 24 2022 at 01:41):

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

Arien Malec (Nov 24 2022 at 01:43):

That’s the one…

Jason Rute (Nov 24 2022 at 01:51):

@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 (Nov 24 2022 at 01:57):

@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 (Nov 24 2022 at 02:09):

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

Arien Malec (Nov 24 2022 at 03:22):

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 (Nov 24 2022 at 06:47):

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 (Nov 24 2022 at 06:48):

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 (Nov 24 2022 at 12:29):

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 (Nov 24 2022 at 12:33):

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 (Nov 24 2022 at 14:05):

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 (Nov 24 2022 at 14:06):

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

Bhavik Mehta (Nov 24 2022 at 14:06):

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

Pedro Sánchez Terraf (Nov 24 2022 at 15:39):

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 (Nov 24 2022 at 15:47):

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 (Nov 24 2022 at 15:49):

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

Arien Malec (Nov 24 2022 at 15:51):

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

David Thrane Christiansen (Nov 26 2022 at 13:02):

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 (Nov 26 2022 at 13:05):

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 (Nov 28 2022 at 18:42):

Just came across this & it’s quite good

Arien Malec (Nov 28 2022 at 18:42):

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

James B Clifford (Dec 06 2022 at 03:02):

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

Tyler Josephson ⚛️ (Dec 08 2022 at 14:43):

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

Arthur Paulino (Dec 09 2022 at 11:30):

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


Last updated: Dec 20 2023 at 11:08 UTC