New release of Functional Programming in Lean

Stream: lean4

[David Thrane Christiansen]

The second release of Functional Programming in Lean is up. This release completes Chapter 1. As always, feedback is more than welcome here or via email.

I hope you find it useful! It's available at https://leanprover.github.io/functional_programming_in_lean/ .

[David Thrane Christiansen]

Hello again! The third release is up. It contains Chapter 2, which describes IO, lake, and introduces do-notation.

[Mac]

@David Thrane Christiansen One note: the feline example could use lake new feline exe instead to generate just an executable configuration.

[František Silváši]

I love the way you introduce IO actions, no monoids in the category of endofunctors, no algebraic effects; 10/10 :).
A few very minor observations:
a) 2.1 - Anatomy of a Greeting

Because this action doesn't read any interesting information from the environment in the process of emitting the string, IO.println has type String → IO Unit

I don't think it's immediately obvious as to what the type would be if it did indeed read anything interesting from the environment, but perhaps it's just my inability to process the sentence properly :).

b) 2.2 - IO Actions vs Values

It's structure....

Just a typo from 'Its structure'.

c) 2.4 - Main
This is more so a nitpick and realistically completely irrelevant in a Lean book, but in specifically C (and rules are different in C++):
0) you'll never see a standard-compliant main that returns void unless you want to rely on /* or in some other implementation-defined manner. */ in the standard
1) technically, any function in C that does not specify void in the parameter list takes any number of arguments; as such, especially main should be explicitly labelled as int main(void) if you want the one that takes no arguments

[Tom]

The counter worker/cook analogy is really nice but it threw me off a bit upon first reading and I had to do a mental "flip" when I reached the conclusion.

Once I got to the end of the paragraph it was clear the counter worker is the IO monad that interacts with the real world but my expectation reading initially was exactly the opposite: I, the client, am interacting with the nice/clean/polite and friendly counter worker Lean (it also made sense in the sense of requesting what I want, i.e. being declarative) while, behind the scenes, the cook (the runtime) does all the "heavy lifting".

[David Thrane Christiansen]

Mac said:

David Thrane Christiansen One note: the feline example could use lake new feline exe instead to generate just an executable configuration.

Thanks! I'll consider revising it. I think there's some value in people editing the file, just to get the experience, but it's also nice to show the available conveniences.

[David Thrane Christiansen]

@František Silváši I've created an issue on my tracker to make sure I follow up on these points - they'll be fixed in the next release. Thank you! And given that C has a strong culture of reading and adhering to standards, rather than just what implementations actually do, I think it's important to respect it so as not to lose C programmers who are less sold on Lean. This feedback is very valuable (as are the other points), so thank you very much!

[David Thrane Christiansen]

@Tom thanks for the feedback! I'll think a bit more about that analogy.

[Patrick Massot]

I like the analogy and I read it correctly from the beginning but of course I already know about monads. David, maybe you could simply insert a stronger hint at the very beginning clarifying who is the cook and who is the counter worker.

[Paul Chisholm]

A couple of comments on chapter 1:

• 1.6 Polymorphism-Option
  Might be worth mentioning coercion allows the body of List.head? to be written

  match xs with
  | [] => none
  | y :: _ => y

and Lean infers the y really means some y. This may be a little advanced for an introductory text, but it is the sort of thing that could catch out newcomers from languages where the some is mandatory. Perhaps it would be better in the Additional Conveniences section.

• 1.7 Additional Conveniences
  Would be worth mentioning that match cases can be combined when the expression on the RHS is the same, so the halve example can be written:

def halve : Nat → Nat
  | 0
  | 1 => 0
  | n + 2 => halve n + 1

[Paul Chisholm]

Another couple of things it would be good to cover:

• The difference between = and == (even if just to note == is used for the moment and = will be explained in From Programming to Proving).
• Explanation of the .name notation where Lean infers the namespace from context (I see this in a couple of the examples and in Zulip topics, but not in the documentation yet that I have observed).

[Henrik Böving]

Note that we would usually write

def halve : Nat -> Nat
  | 0 | 1 => 0
  | n + 2 => halve n + 1

Not splitting the combined case out over multiple lines

[David Thrane Christiansen]

@Paul Chisholm thanks for the feedback!

Lean infers the y really means some y

I'm intentionally avoiding all coercions until the feature can be explained properly. Lean has so many features that their interactions can be quite overwhelming even for people with deep experience with proof assistants and functional programming, and this text is intended for readers with zero experience in either. I need to be careful in how much they get in chapter 1, but coercions are absolutely on the radar for later in the book, and this is a good example.

[David Thrane Christiansen]

I've created issues in my repository tracking each of the points that you brought up. I think that Ch1 is already longer than it should be, but it's certainly important to get to all of them at some point. Thanks again!

[Paul Chisholm]

@David Thrane Christiansen Thanks for the response. The book is shaping up nicely. I think it will be an invaluable resource for Lean programming.
@Henrik Böving That formatting makes sense. Is there, or is there planned, a Lean style guidelines, or even an automated code formatter?

[Henrik Böving]

The plan is to eventually get the delaborator to a point where it can act as a pretty printer for Lean. However right now it isn't even guaranteed to produce things that typecheck/evaluate to the same thing as their input properly so that is still a long way to go but we have people investigating and working on the issue right now.

[David Thrane Christiansen]

@František Silváši 🦉 Thanks again for the comment! I've fixed the issues you identified on my main branch, and the corrections will find their way into the imminent release.

[David Thrane Christiansen]

It's that time again! There's a fresh release of Functional Programming in Lean available for your reading pleasure. This time around, the first half of the type class chapter is available. It's later than usual this month due to my summer vacation and ICFP, but releases will be returning to the usual schedule next month.

As usual, feedback is welcome both here and in my email. Thank you for reading it!

[Tom]

Thank you!

Very minor nit: On the first page, you write:

an instance is created that contains an implementation of each operation for the new type. For instance, a type class named Add

I wonder if in this case the second instance :upside_down: of the world "instance" (emphasis mine) would be better served with "example" for clarity's sake. (This also re-occurs later in the chapter)

[Paul Chisholm]

Good description of type classes.

A few minor typos:

• 3.1, Overloaded Addition, second paragraph. "While an understanding the full..." -> "While an understanding of the full..."
• 3.1, Overloaded Multiplication, first paragraph. "...with the same time" -> "...with the same type"
• 3.1, Literal Numbers, second last paragraph. Missing '.' at end of the second sentence, immediately before 'Just'.
• 3.2, Methods and Implicit Arguments, first paragraph. "because the declaring a" -> "because declaring a"
• 3.2, Methods and Implicit Arguments, third paragraph. ""In order for the Lean" -> "In order for Lean"
• 3.3, Heterogenous Overloadings, second paragraph. "For instance, given the above two instances..." -> "Given the above two instances...". The repeated use of 'instance' seems awkward.

[František Silváši 🦉]

This reads very coherently, I genuinely like this.

I have two notes that are of stylistic nature and can be safely disregarded :).
0) In 3.1. - open Plus (plus) the 'selective export of plus' feature is first introduced (unless I am misremembering!) here, which is a section 'Classes and Instances'; it feels to me a little bit buried here if this is to be the first exposition to the feature. Maybe its first mention in 2.3. 'Libraries and Imports' might be a nicer place.

1) In 3.1. - 'Conversion to Strings', in the context of:

Additionally, if a type has a ToString instance, then it can be used to display the result of #eval...

This is, to me, begging for a short explanation of the difference between Repr and ToString, but I can also imagine this being elsewhere (or not present at all :)), as there are admittedly better contexts for this.

Again, this is very much a 'personal take', do feel more than encouraged to ignore this, there's nothing wrong with either of these :).

[David Thrane Christiansen]

@Paul Chisholm I've fixed all those in the latest version, thanks! And sorry it took me a bit to get back to you here.

[David Thrane Christiansen]

@František Silváši 🦉 These are very good suggestions that I've put into the book's issue tracker.

[David Thrane Christiansen]

Halloween is approaching, but there's no need to be afraid of proofs or of type classes.

A new release of Functional Programming in Lean is up, containing the rest of the chapter on type classes as well as updates based on your excellent feedback. This release also contains a short interlude that lightly introduces the idea of propositions, proofs, and truth, because they were really necessary in order to explain things like GetElem.

As always, your feedback is much appreciated.

[Patrick Massot]

In https://leanprover.github.io/functional_programming_in_lean/type-classes/coercion.html, the last section seems outdated since CoeHead and CoeTail are discussed in this chapter.

[Patrick Massot]

A very minor point: in several places you use tree names as examples, but this will add completely unnecessary friction for people whose native language isn't English. I have no idea what is a birch or a beech. I understand that it doesn't matter, but it still slows me a tiny bit while reading.

[Patrick Massot]

In https://leanprover.github.io/functional_programming_in_lean/type-classes/coercion.html, there is an inconsistency betwenn howMany and howMuch.

[Patrick Massot]

In https://leanprover.github.io/functional_programming_in_lean/type-classes/pos.html#another-representation I don't understand the example, but maybe I forgot a previous explanation of this syntax.

[Patrick Massot]

Oh I see: this is the syntax to overload the constructor name, right? I always forget about this possibility.

[František Silváši 🦉]

Another good chapter :).

Minor notes - once again, really just stylistic (in addition to what Patrick's already mentioned):

In 4.5 - Equality and Ordering, in the context of:

From the perspective of mathematics, two functions are equal if they map equal inputs to equal outputs, so this statement is even true, though it requires a two-line proof to convince Lean of this fact.

Mathematics doesn't technically 'need to' do extensional, it's just the common set-theoretic one; might be worth rephrasing.

In 4.6 - Chaining Coercions:
There's a mention of CoeHead that's like: oh yeah, this exists. I would actually be interested in seeing an example of where this is useful, because frankly, I can't think of one and a quick grep of the Lean 4 repo comes up with a single instance of this, some deep in Syntax that's far from immediately straightforward to understand.

In 4.6 - Design Considerations

'First off,coercion' - typo, space after comma

Very enjoyable read btw.

[Arien Malec]

Thanks for this!

In the coercions chapter should the need to tag coercion methods with @[coe] be mentioned? I'm not clear on when that attribute is required but I do know that it can trip one up.

[Patrick Massot]

František Silváši 🦉 said:

In 4.5 - Equality and Ordering, in the context of:

From the perspective of mathematics, two functions are equal if they map equal inputs to equal outputs, so this statement is even true, though it requires a two-line proof to convince Lean of this fact.

Mathematics doesn't technically 'need to' do extensional, it's just the common set-theoretic one; might be worth rephrasing.

At the level of detail of this book about mathematics, I think it is really pointless to mention that some extremely specialized areas of mathematics need more refined versions of function equality. This has nothing to do with foundations of mathematics, it is simply the meaning of the word function in informal real world mathematics.

[František Silváši 🦉]

I don't necessarily disagree; that doesn't mean the sentence can't be phrased in a slightly different way that also includes the fact that this is 'merely' the most common interpretation. Of course, this is exceedingly minor :).

[David Thrane Christiansen]

@Patrick Massot Thanks for all the great suggestions! I've fixed the errors in the development version of the book, and I added a little reminder about the structure constructor syntax in the exercise. WRT the tree names: I realy don't want to use lists of numbers, as my experience is that meaningful examples are much more meaningful for most people. But it sounds like picking trees from my local ecosystem is not a good solution for a big population of readers, so I'll think about some different themes to use (or at least drop some of the more similar-sounding ones).

[David Thrane Christiansen]

@František Silváši 🦉 : I'm aiming for a level of mathematics background here that is quite low. Just as I'm not planning on having an extensive discussion of constructive vs classical reasoning (except just enough to talk about computable vs noncomputable definitions), I'm not planning on talking about intensional vs extensional characterizations of functions or any such thing. I'll be mostly just appealing to the ideas of sets and functions that people learn when they're 13 years old, because that's not what this is about. I suspect that anyone with the background to stumble over this will also be in a position to realize that they're at a different level.

Thanks!

[David Thrane Christiansen]

Arien Malec said:

Thanks for this!

In the coercions chapter should the need to tag coercion methods with @[coe] be mentioned? I'm not clear on when that attribute is required but I do know that it can trip one up.

I'm actually not aware of that attribute! I can't find any instances of it in the Lean source code. Can you point me to some information so I can investigate? Thanks!

[Arien Malec]

Here’s the thread where I ran into the coercion registration issue:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/norm_cast.20not.20seeing.20coercion.3F

[Petar Maymounkov]

I am following _Functional programming in lean_ and trying to define a basic type which is ordered.
I am puzzled as to why I get an error when I try to evaluate the < operator:

inductive Bit where
   | zero : Bit
   | one : Bit

open Bit

def Bit.compare (x y : Bit) : Ordering :=
   match (x, y) with
   | (zero, zero) => Ordering.eq
   | (zero, one) => Ordering.lt
   | (one, zero) => Ordering.gt
   | (one, one) => Ordering.eq

instance : Ord Bit where
   compare := Bit.compare

#eval zero < zero -- <- failed to synthesize

[Notification Bot]

This topic was moved here from #lean4 > instantiating Ord and "failed to synthesize instance" by Petar Maymounkov.

[Sebastian Ullrich]

Currently Ord does not automatically imply LT (which powers <). This is likely to improve soon: https://github.com/leanprover/lean4/issues/1777

[Sebastian Ullrich]

You can use

instance : LT Bit := ltOfOrd

for now

[Petar Maymounkov]

Sebastian Ullrich said:

Currently Ord does not automatically imply LT (which powers <). This is likely to improve soon: https://github.com/leanprover/lean4/issues/1777

But I have the same issue with LT:

inductive Bit where
   | zero : Bit
   | one : Bit

open Bit

def Bit.lt (x y : Bit) : Prop :=
   match (x, y) with
   | (zero, zero) => false
   | (zero, one) => true
   | (one, zero) => false
   | (one, one) => false

instance : LT Bit where
   lt := lt

#eval zero < zero -- <-- fail

[Sebastian Ullrich]

Ah, you cannot #eval propositions - they don't have a value. Lean is trying to be helpful and convert it to a Bool using the Decidable typeclass, but there is no instance of that for Bit. If you use ltOfOrd as above, you get a Decidable instance for free.

[Sebastian Ullrich]

def Bit.lt (x y : Bit) : Bool :=  -- Bool!
   match (x, y) with
   | (zero, zero) => false
   | (zero, one) => true
   | (one, zero) => false
   | (one, one) => false

instance : LT Bit where
   lt a b := lt a b

also works fwiw

[Mario Carneiro]

Is that true? I think you still have to register it

[Mario Carneiro]

it is true

instance : Ord Bit where
   compare := Bit.compare

instance : LT Bit := ltOfOrd

#eval zero < zero -- works

[Sebastian Ullrich]

https://github.com/leanprover/lean4/blob/999b61007cbae0cad15172fcad5cffba43c13488/src/Init/Data/Ord.lean#L71-L72

[Sebastian Ullrich]

Since we're already using ltOfOrd, it's fine to infer the rest

[Mario Carneiro]

I would have thought that declaring the instance would make that instance not apply anymore since it is wrapped

[Mario Carneiro]

that is, here:

instance myLt : LT Bit := ltOfOrd

we would end up with Decidable (@LT.lt Bit myLt) instead of Decidable (@LT.lt Bit ltOfOrd)

[Sebastian Ullrich]

Typeclass inference unfolds reducibles and instances

[David Thrane Christiansen]

Arien Malec said:

Here’s the thread where I ran into the coercion registration issue:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/norm_cast.20not.20seeing.20coercion.3F

As far as I can tell, this is a mathlib4 concern, rather than one of Lean per se. Mathlib4 is explicitly out of scope for this book. But thanks!

[eyelash]

I noticed something minor in chapter 4.4:

much like a Java ArrayList, a C++ std::vector, or a Rust std::vec.

The data structure in Rust is actually called Vec (with an upper case V), std::vec is just the module where that data structure is defined. std::vec::Vec is also part of the prelude so it probably makes sense to refer to it as just Vec.

[eyelash]

I also find the sentence "arrays occupy a contiguous region of memory, which is much better for processor caches" a bit confusing since AFAIK (someone please correct me if I'm wrong) the values of the array are still boxed in Lean, so only the pointers are stored in a contiguous region, especially after the comparison to C++ and Rust where the values themselves are actually stored in a contiguous region of memory.

[James Gallicchio]

Scalars will be stored unboxed. But, yeah, many objects are boxed P:

[Arien Malec]

@David Thrane Christiansen none of that code depended on Mathlib4

[David Thrane Christiansen]

eyelash said:

I noticed something minor in chapter 4.4:

much like a Java ArrayList, a C++ std::vector, or a Rust std::vec.

The data structure in Rust is actually called Vec (with an upper case V), std::vec is just the module where that data structure is defined. std::vec::Vec is also part of the prelude so it probably makes sense to refer to it as just Vec.

Thanks! I fixed this in the latest development release.

[David Thrane Christiansen]

eyelash said:

I also find the sentence "arrays occupy a contiguous region of memory, which is much better for processor caches" a bit confusing since AFAIK (someone please correct me if I'm wrong) the values of the array are still boxed in Lean, so only the pointers are stored in a contiguous region, especially after the comparison to C++ and Rust where the values themselves are actually stored in a contiguous region of memory.

This is a good point, so I've created an issue to track it.

[David Thrane Christiansen]

Arien Malec said:

David Thrane Christiansen none of that code depended on Mathlib4

As far as I can see, that attribute only exists in mathlib4. But I'll ask about it next time I talk to Lean developers on the phone - I could very well be overlooking something.

[Sebastian Ullrich]

It's in std4 now docs4#Tactic.NormCast.Attr.coe

[Evgenia Karunus]

In https://leanprover.github.io/functional_programming_in_lean/type-classes/coercion.html #eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString the .asString call doesn't work for me with the environment does not contain 'JSON.asString'.

[David Thrane Christiansen]

eyelash said:

I also find the sentence "arrays occupy a contiguous region of memory, which is much better for processor caches" a bit confusing since AFAIK (someone please correct me if I'm wrong) the values of the array are still boxed in Lean, so only the pointers are stored in a contiguous region, especially after the comparison to C++ and Rust where the values themselves are actually stored in a contiguous region of memory.

I fixed this in the latest development version. It's now more clear that it's referring to the array itself being in a contiguous block, rather than having a pointer at each node like a linked list. Thanks again!

[David Thrane Christiansen]

Evgenia Karunus said:

In https://leanprover.github.io/functional_programming_in_lean/type-classes/coercion.html #eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString the .asString call doesn't work for me with the environment does not contain 'JSON.asString'.

Thanks for this. The implementation of JSON.asString is a bit hairy, so I was hoping to get away with not having it along. I'll beautify it and add it in the next release.

[David Thrane Christiansen]

The November release is out at https://leanprover.github.io/functional_programming_in_lean/ ! The new chapter covers monads, and I'm now hard at work on writing about monad transformers.

Thank you all for your ongoing support and feedback, the book is much improved by your comments.

[Arien Malec]

The way you present the motivation in terms of obvious patterns before using the "M" word is lovely.

[David Thrane Christiansen]

Thanks! The M-word is scary for people who haven't seen it before, and experience in classrooms has made it crystal clear to me that most people do better seeing examples before definitions, so that's how I tried to write it.

[Kevin Buzzard]

Did you take a look at "programming in Lean"? This is a half-finished lean 3 book from five years ago which taught me what a monad was (by going through four examples). I suspect Jeremy wrote it, he's good at writing stuff which teaches me things

[Jeremy Avigad]

Yup, that was me. Bas Spitters once told me that the reason that there are so many monad tutorials online is that everyone who finally understands them is so proud of themselves that they are compelled to write a tutorial. I visited Microsoft in the summer of 2016 and I learned how to use monads. I was so proud of myself that I wrote a tutorial.

[David Thrane Christiansen]

For some of the readers I want to reach, I think that the definition-first approach taken in his book will not work as well as the example-first approach that I'm going for here. I'm also intentionally trying to avoid mathematical jargon, though I didn't entirely succeed :-)

[Moritz Doll]

I've had a brief look and I think the example first approach is very good. Even though I am a mathematician by training I hate all of the 'monads are a part of category theory' nonsense, since it does not help you to understand anything and I was slightly sad that keeps appearing.

[David Thrane Christiansen]

Ideally, there are different learning resources for different audiences, adapted to their specific needs. I know people who learned Haskell after knowing a fair bit of category theory already, and they had quite different challenges in learning to program with monads than most people!

Programming with monads requires approximately zero category theory, just as you really don't need to know any graph theory to implement A* search for pathfinding in a game.

[Patrick Massot]

I think this chapter still lacks an introduction warning readers that you will first solve a problem in a very painful way for the sake of motivating some abstract gadget. Otherwise innocent readers will simply be terrified by the first examples.

[Patrick Massot]

And, as far as I remember, Jeremy's explanation doesn't feature any category theory.

[Mario Carneiro]

It might also help to give people a taste of what the final result is, since otherwise it's not really clear where it is all going. The endpoint of the Option example is not really that satisfactory:

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  xs[4]? ~~> fun fifth =>
  xs[6]? ~~> fun seventh =>
  some (first, third, fifth, seventh)

I sure am glad I don't have to write that and can do this instead:

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) := do
  return (← xs[0]?, ← xs[2]?, ← xs[4]?, ← xs[6]?)

[Arien Malec]

Patrick Massot said:

I think this chapter still lacks an introduction warning readers that you will first solve a problem in a very painful way for the sake of motivating some abstract gadget. Otherwise innocent readers will simply be terrified by the first examples.

well the handrolled Monadic functions specialized to Option, etc. is exactly how Rust gets on, with some special ? syntax for Option and Result where short circuiting on failure is what's wanted. And and the piles of nested function calls is exactly how Promise based async code used to work in JS until everyone borrowed async/await from C# which ultimately was from…Haskell (via Simon Marlow).

[Jireh Loreaux]

Mario, the only difference between what appears in the book and your example is some syntactic sugar right? In that case, I think an easy fix without breaking too much the flow would be to add this right before the section Logging:

"In Section 5.3 we'll learn some that we have some syntactic sugar which can simplify this even further to:

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) := do
  return (← xs[0]?, ← xs[2]?, ← xs[4]?, ← xs[6]?)

But for now we'll postpone explanation of this syntax in order to consider several more examples."

This succinct version should then also be included in Section 5.3. (@David Thrane Christiansen of course, these are only suggestions!)

[David Thrane Christiansen]

These are great suggestions, thanks everyone!

[Sebastian Ullrich]

I saw a certain trend on Mastodon today, I wonder if it's helpful here as well...

ChatGPT on "write biblical verses in the style of the king james bible in the form of a rap explaining the concept of monads from functional programming"

Verse 1:

In the beginning, God created the code
And with it, the concept of monads bestowed
A way to compose functions in a pure mode
A building block for functional programming, it bode

Chorus:

Monads, monads, the building blocks of code
A way to create functional flows
An abstract concept, but one that we must hold
For the power of functional programming to unfold

Verse 2:

Monads allow us to bind and chain
Functions together, without causing pain
To the purity of the code, we remain
As monads ensure our functions remain the same

Chorus:

Monads, monads, the building blocks of code
A way to create functional flows
An abstract concept, but one that we must hold
For the power of functional programming to unfold

Bridge:

Monads may seem complex at first glance
But with study and practice, they will enhance
Your understanding of functional programming's advance
And open up new possibilities in your code's expanse

Chorus:

Monads, monads, the building blocks of code
A way to create functional flows
An abstract concept, but one that we must hold
For the power of functional programming to unfold

[František Silváši 🦉]

Another chapter written with a very good 'flow' to it :). Maybe introducing the way of creating infix notations in a chapter 'Monad' is not ideal, but I understand it's very much on 'needed now' bases. This book is excellent.

[David Thrane Christiansen]

Hi everyone! There's a new release out at https://leanprover.github.io/functional_programming_in_lean/, with a chapter on Applicative that takes a few necessary detours through universe polymorphism and structure inheritance. I haven't yet made the improvements suggested up-thread, but they're certainly on the radar still. Thanks again for reading!

[David Thrane Christiansen]

Next up is monad transformers. It's already half written, but I realized that I needed to already have Applicative to make progress so I backtracked a bit :-) It was a busy December.

[Marcus Rossel]

In Universes > Prop and Polymorphism:

Prop is at the bottom of the universe hierarchy, and the type of Prop is Type. This means that lists of propositions have type List Type:

def someTruePropositions : List Prop := [
  1 + 1 = 2,
  "Hello, " ++ "world!" = "Hello, world!"
]

... should the "have type List Type" actually be "have type List Prop"?

[Henrik Böving]

Yes it should be i think.

[Yaël Dillies]

The fact that Prop : Type is irrelevant here, I think

[David Thrane Christiansen]

Marcus Rossel said:

In Universes > Prop and Polymorphism:

Prop is at the bottom of the universe hierarchy, and the type of Prop is Type. This means that lists of propositions have type List Type:

def someTruePropositions : List Prop := [
  1 + 1 = 2,
  "Hello, " ++ "world!" = "Hello, world!"
]

... should the "have type List Type" actually be "have type List Prop"?

Nice catch!

[David Thrane Christiansen]

All right, it's fixed in the development release of the book. Thanks again!

[Yaël Dillies]

In the section on types, it looks like this sentence is missing a word: To use a type that can represent the negative integers, provide a it directly:

[Yaël Dillies]

In functions and definitions, I think you meant

so the preceding function types can be written `Nat -> Nat` and `Nat -> Nat -> Nat`, respectively.

rather than

so the preceding function types can be written `Nat -> Bool` and `Nat -> Nat -> Nat`, respectively.

[Yaël Dillies]

In Polymorphism, Just as C# and Java require type arguments to provided explicitly should be Just as C# and Java require type arguments to be provided explicitly

[Arien Malec]

I think it would be helpful to note that while you are working through inheritance of structures, it generally better to use typeclasses rather than structural inheritance to encapsulate common behavior.

[David Thrane Christiansen]

Yaël Dillies said:

In the section on types, it looks like this sentence is missing a word: To use a type that can represent the negative integers, provide a it directly:

Thanks! It was actually just a spurious "a", which is now deleted.

[David Thrane Christiansen]

Yaël Dillies said:

In functions and definitions, I think you meant

so the preceding function types can be written `Nat -> Nat` and `Nat -> Nat -> Nat`, respectively.

rather than

so the preceding function types can be written `Nat -> Bool` and `Nat -> Nat -> Nat`, respectively.

Thanks! I've fixed it. This was one of the few types shown in the book that wasn't machine-checked - I've rectified that now :-)

[David Thrane Christiansen]

Yaël Dillies said:

In Polymorphism, Just as C# and Java require type arguments to provided explicitly should be Just as C# and Java require type arguments to be provided explicitly

This is now fixed as well. Thank you for your sharp eyes and careful attention!

[David Thrane Christiansen]

Arien Malec said:

I think it would be helpful to note that while you are working through inheritance of structures, it generally better to use typeclasses rather than structural inheritance to encapsulate common behavior.

This is a good note to have somewhere, but I don't think it should be there because inheritance of type classes has not yet been introduced. I'll think about the right place to put it, along with a way of explaining why.

[František Silváši 🦉]

You know a chapter is great when 'the best' people can find is minor typos! :)

• 6.2: Checking whether an [sic] value of type α is in the subtype...
• 6.7: Defining a class defines a structure, and additionally creates a [sic] empty table of instances...

[David Thrane Christiansen]

František Silváši 🦉 said:

You know a chapter is great when 'the best' people can find is minor typos! :)

• 6.2: Checking whether an [sic] value of type α is in the subtype...
• 6.7: Defining a class defines a structure, and additionally creates a [sic] empty table of instances...

:embarrassed: I should have caught those proofreading! Sorry, and thanks for the kind way of pointing them out :-)

[Yaël Dillies]

• 2.6 : Missing s in While most language allow
• 3. : The sentence Computer-aided theorem provers like Lean are designed to allow mathematicians to write proofs while omitting many details, while the software fills in the missing explicit steps, decreasing the likelihood of oversights or mistakes. reads a bit heavy. Maybe because of the duplicated "while"?
• 3. propositions are a kind of type. I know "type" is referring to p : Prop, but it could be misread as meaning Prop because of the singular

[Jireh Loreaux]

David Thrane Christiansen said:

This is a good note to have somewhere, but I don't think it should be there because inheritance of type classes has not yet been introduced. I'll think about the right place to put it, along with a way of explaining why.

How about a footnote, possibly with a forward reference?

[David Thrane Christiansen]

Yaël Dillies said:

• 2.6 : Missing s in While most language allow
• 3. : The sentence Computer-aided theorem provers like Lean are designed to allow mathematicians to write proofs while omitting many details, while the software fills in the missing explicit steps, decreasing the likelihood of oversights or mistakes. reads a bit heavy. Maybe because of the duplicated "while"?
• 3. propositions are a kind of type. I know "type" is referring to p : Prop, but it could be misread as meaning Prop because of the singular

Thanks, these are fixed in the development branch!

[David Thrane Christiansen]

Jireh Loreaux said:

How about a footnote, possibly with a forward reference?

I don't think footnotes work well in writing that's intended to be consumed online - they end up being a bit like endnotes in paper books, where they're so inconvenient to consult that they might as well not be there. And Markdown/mdbook unfortunately doesn't have reasonable support for asides, marginalia, or other things that work well for this task.

I'll puzzle over it.

[Jireh Loreaux]

Footnotes with return hyperlinks (generally denoted by a ↩) I find to be easily read even online, but it's fine if you disagree. Dealing with non-linearity of topics is always hard.

[Ian Young]

I haven't really got this far yet*, but while I was reading ahead, I noticed that in 6.2 Applicative Functors: Validated Input the code block following "Finally, these three components can be combined using seq:" is the same as the previous code block, whereas the following text implies that it should define checkInput.

*I'm finding myself a bit confounded by the Even Number Literals exercise in 4.2. But that's another story.

[David Thrane Christiansen]

Thanks for catching the mistake! It's now fixed in the development branch and will be out in the next release. The code should read:

def checkInput (year : Nat) (input : RawInput) : Validate (Field × String) (CheckedInput year) :=
  pure CheckedInput.mk <*>
    checkName input.name <*>
    (checkYearIsNat input.birthYear).andThen fun birthYearAsNat =>
      checkBirthYear year birthYearAsNat

[David Thrane Christiansen]

Here's a hint for even number literals: it's using recursive instance search, so you're going to want one instance that is the base case for the search, and another instance that takes a literal for some smaller Even (via finding an OfNat for that smaller Even) and transforms it into a literal for a somewhat larger Even.

Start with your base case: it should give a literal for the smallest Even number. Get that working first.

[Ian Young]

@David Thrane Christiansen Thanks for the hint. That was what I'd thought I tried, but it fails to synthesize an instance for values larger than 0:

inductive Even : Type where
  | zero : Even
  | succ2 : Even → Even

def Even.toNat : Even → Nat
  | Even.zero => 0
  | Even.succ2 n => n.toNat + 2

instance : ToString Even where
  toString x := toString (x.toNat)

instance : OfNat Even 0 where
  ofNat := Even.zero

instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.succ2 (OfNat.ofNat n)

#eval (0: Even)
#eval (2: Even)

What's particularly confusing me is that the very similar definition in this thread clearly does work, and adapting that I can get this:

inductive GEven : Nat → Type where
  | zero : (m : Nat) → GEven m
  | succ2 : {m : Nat} → GEven m → GEven m

instance : OfNat (GEven m) m where
  ofNat := GEven.zero m

instance [OfNat (GEven m) n] : OfNat (GEven m) (n + 2) where
  ofNat := GEven.succ2 (OfNat.ofNat n)

abbrev Even : Type := GEven 0

#check (0 : Even)
#check (2 : Even)

Which works, but seems a bit mad! Clearly my first attempt isn't allowing it to 'chain together' the base and recursive cases, but I don't see why not.

[David Thrane Christiansen]

Try replacing instance : OfNat Even 0 where with instance : OfNat Even Nat.zero where. That works for me, at least - I should figure out and describe this gotcha!

[David Thrane Christiansen]

Your latter example has some aspects that don't make sense to me - the succ2 constructor doesn't add two anywhere, for instance, and the zero constructor seems to say that every Nat is even. Then your first instance of OfNat should work for any Nat literal at all, even odd ones. The second instance doesn't relate m to n+2 in any way.

[Ian Young]

Yes, using Nat.zero instead of 0 there works for me. Thanks!

My second attempt made sense to me (except for its over-complication): GEven m represents even numbers from m upwards (in the same way as GNat n in the referenced thread represents natural numbers from n upwards).

[Ian Young]

What I don't think I was expecting is that with either of these definitions, #check (254 : Even) works, but #check (256 : Even) just says "failed to synthesize instance OfNat Even 256". Given the point at which it fails, I presume the latter case is 'running out of gas'?

[David Thrane Christiansen]

That seems like the right explanation - another TODO for the book! Thanks!

[David Thrane Christiansen]

The thing about your GEven example is that it seems to me that it also represents odd numbers when m is odd. In particular,

example : GEven 1 := .zero 1

If I wanted to write an inductive family to represent only the even numbers greater than or equal to some given number, I'd want to do something like:

inductive GEven (basis : Nat) : Nat → Type where
  | base : basis % 2 = 0 → GEven basis basis
  | plusTwo : GEven basis n → GEven basis (n + 2)

The issues with your version are:

1. It doesn't ensure that the base number is even
2. It doesn't track the actual Nat

The second issue could be solved pretty well by having a function that converted it to a Nat. But the first one really does need the k % 2 = 0 bit on the base case.

Here's a proof that the version here represents even numbers greater than or equal to some base number:

theorem geven_is_even (n : Nat) (even : GEven basis n) : n % 2 = 0 := by
  induction even <;> simp [*]
  case plusTwo _ ih =>
    have step (n : Nat) : (n + 2) % 2 = n % 2 := by
      have : (n + 2) % 2 = if 0 < 2 ∧ 2 ≤ n + 2 then (n + 2 - 2) % 2 else n + 2 := Nat.mod_eq (n + 2) 2
      have : 2 ≤ n + 2 := by simp_arith
      simp [*, Nat.add_sub_self_right n 2]
    simp [*]

theorem geven_is_ge (n : Nat) (even : GEven basis n) : n ≥ basis := by
  simp_arith
  induction even <;> simp
  case plusTwo _ ih =>
    constructor; constructor; assumption

The other version that doesn't track the specific even Nat at the type level works basically the same way:

inductive GEven (basis : Nat) : Type where
  | base : basis % 2 = 0 → GEven basis
  | plusTwo : GEven basis → GEven basis

def GEven.toNat : GEven k → Nat
  | .base _ => k
  | .plusTwo more => toNat more + 2

theorem geven_is_even (even : GEven basis) : even.toNat % 2 = 0 := by
  induction even <;> simp [*]
  case plusTwo _ ih =>
    simp [GEven.toNat]
    have step (n : Nat) : (n + 2) % 2 = n % 2 := by
      have : (n + 2) % 2 = if 0 < 2 ∧ 2 ≤ n + 2 then (n + 2 - 2) % 2 else n + 2 := Nat.mod_eq (n + 2) 2
      have : 2 ≤ n + 2 := by simp_arith
      simp [*, Nat.add_sub_self_right n 2]
    simp [*]

theorem geven_is_ge (even : GEven basis) : even.toNat ≥ basis := by
  simp_arith
  induction even <;> simp [GEven.toNat]
  case plusTwo _ ih =>
    constructor; constructor; assumption

They're so similar because the constraints that the indexed family imposes on the index are precisely the computation behavior of GEven.toNat in this case.

[Ian Young]

Sorry, I seem to have wasted your time here with an offhand remark. The point of my GEven was just to get an answer to the exercise after my original attempt didn't work.

[David Thrane Christiansen]

Don't worry - it was fun :-)

[Ian Young]

Moving on to 4.3. Controlling Instance Search: Default Instances:

instance [Add α] : HPlus α α α where
  hPlus := Add.add

With this instance, hPlus can be used for any addable type, like Nat:

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

Shouldn't this #eval have two Nat arguments?

[Ian Young]

In 4.4. Arrays and Indexing: Non-Empty Lists

For example, the non-empty list idahoSpiders (which contains some spider species native to the US state of Idaho) consists of "Banded Garden Spider" followed by four other spiders, for a total of five spiders.

Were you intending this to be followed by such a definition? From the later examples (in 4.5. Standard Classes: Appending), it's clearly just:

def idahoSpiders : NonEmptyList String :=
  { head := "Banded Garden Spider",
    tail := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced Spider"] }

But it breaks the flow if I have to go looking for spiders to put in the list... and then I'll get distracted, wondering why you didn't include the bold jumping spider Phidippus audax, because, let's face it, jumping spiders are the best!

[David Thrane Christiansen]

I'll check those out, thanks!

[David Thrane Christiansen]

The January release is now out, featuring monad transformers and fancy do-notation features!

[Floris van Doorn]

7.1 typo: "Files whose names being" -> "Files whose names begin"
The section "What counts as a do block?" is very clarifying. I was hesitant using return in nested do-blocks, since I was unsure what block was returning this value.

[Sebastian Ullrich]

Note that your editor should also highlight the corresponding do keyword when you put the cursor on a return statement

[Patrick Massot]

Congratulations @David Thrane Christiansen! The monad transformer chapter is a very nice milestone. It definitely feels like we now have a full book about the core concepts of programming using Lean. Actually I'm not sure what the next chapter will be about.

[Patrick Massot]

Is Chapter 9 meant to be about proving properties of programs written in Lean or theorem proving?

[Patrick Massot]

Do you intend to stop after Chapter 9 or do you want to include a Chapter 10 about interfacing with other programming languages (the famous FFI stuff that seems pretty tricky to setup)? What about giving more advanced explanations about lake?

[David Thrane Christiansen]

Ian Young said:

Shouldn't this #eval have two Nat arguments?

Fixed on the development branch! Thanks!

[David Thrane Christiansen]

Ian Young said:

Were you intending this to be followed by such a definition?

I was, and it's now there. Thank you again!

Ian Young said:

why you didn't include the bold jumping spider Phidippus audax, because, let's face it, jumping spiders are the best!

As far as I can see, they're not native to Idaho. I tried to include nature examples from ecosystems that have been important parts of my life, like Idaho, Cascadia, and southern Scandinavia. They look like cool spiders, though!

[David Thrane Christiansen]

@Patrick Massot The next chapter is intended to be an introduction to programming with indexed families, with things like dependent pattern matching, a repeat of the difference between definitional and propositional equality and why the difference exists, and some of the fun things that dependent types allow in programs. This is a thing that people will not likely have seen elsewhere, and while Lean culture doesn't use it nearly as much as Agda or Idris culture, understanding things like inaccessible patterns is still useful and important.

I was originally going to have 9 be about proofs with tactics _per se_, but I've been outlining and exploring an alternate structure. The alternate structure starts with a discussion of the cost model of Lean programs, describing things like the "immutable beans" optimizations and tail recursion. This naturally leads one to want to write some programs that use arrays mutably (e.g. insertion sort, which is in-place and stable). Many array algorithms are not structurally recursive, which provides a natural hook for talking about termination proofs. These termination proofs are good motivation for proving certain basic things about Nat, and it puts them in a context that's directly useful for programming.

The book will stop after that, at least for now, as the funding that MSR has so generously provided will be running out. I'll be getting Saturdays with my family back :-) Perhaps we'll revisit the collaboration in the future if the book turns out to bring lots of value - I've had fun working on it, at least, though I do need a break. I'll be spending April open-sourcing the infrastructure for CI and examples, proofreading it a couple of times, looking for ways to improve the integration between the sections, checking the exercises for difficulty and distribution, ensuring that there are enough exercises, and so forth.

The reason I sometimes include the wrong example in the book is that I don't write the text as a literate program, because that makes it too hard to get the flexibility I need for the kinds of explanations I want to do. Instead, there's a bunch of Lean macros. So for idahoSpiders, my source file contains:

book declaration {{{ idahoSpiders }}}
  def idahoSpiders : NonEmptyList String := {
    head := "Banded Garden Spider",
    tail := [
      "Long-legged Sac Spider",
      "Wolf Spider",
      "Hobo Spider",
      "Cat-faced Spider"
    ]
  }
stop book declaration

Then the book text (now) contains:

For example, the non-empty list `idahoSpiders` (which contains some spider species native to the US state of Idaho) consists of `{{#example_out Examples/Classes.lean firstSpider}}` followed by four other spiders, for a total of five spiders:
```lean
{{#example_decl Examples/Classes.lean idahoSpiders}}
```

The build script contains some horrid regexp munging that replaces the directives in the text with the associated bits from the text. This allows me to make sure that the text and the examples are always in sync. For things like error messages and #eval output, I have macros that reify the message as a string in the source file and fail if there's a mismatch, like this:

expect error {{{ northernTreesEight }}}
  northernTrees[8]
message
"failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 8 < Array.size northernTrees"
end expect

More regexp magic extracts this to the rendered book. This means that I simultaneously keep error messages in sync with the Lean compiler, and keep the text in sync with the tests.

I think that this use of the metaprogramming system could be useful for others, so I'll definitely open and document it towards the end. I even have a macro for equational reasoning style informal proofs. Here's an example:

namespace MonadApplicativeProof1
axiom m : Type → Type
@[instance] axiom instM : Monad m
@[instance] axiom instLM : LawfulMonad m
axiom α : Type
axiom v : m α

equational steps {{{ mSeqRespId }}}
  pure id >>= fun g => v >>= fun y => pure (g y)
  ={
  by simp [LawfulMonad.pure_bind]
  -- `pure` is a left identity of `>>=`
  }=
  v >>= fun y => pure (id y)
  ={
  -- Reduce the call to `id`
  }=
  v >>= fun y => pure y
  ={
  -- `fun x => f x` is the same as `f`
  }=
  v >>= pure
  ={
  -- `pure` is a right identity of `>>=`
  by simp [LawfulMonad.bind_pure_comp]
  }=
  v
stop equational steps
end MonadApplicativeProof1

The comments contain Markdown that's extracted to the book, and the terms in the middle are checked in a way similar to calc (no term defaults to rfl). This makes it all quite easy to maintain and prevents my scattered brain from skipping important steps.

[David Thrane Christiansen]

That whole equational steps thing is actually quite simple to implement too:

declare_syntax_cat eqSteps

syntax term : eqSteps
syntax term "={" "}=" eqSteps : eqSteps
syntax term "={" term "}=" eqSteps : eqSteps

syntax withPosition("equational" "steps" "{{{" ws ident ws "}}}" (colGt eqSteps) "stop" "equational" "steps") : command

inductive Steps where
  | done : Lean.Syntax → Steps
  | cons : Lean.Syntax → Option Lean.Syntax → Steps → Steps

def Steps.process [Monad m] (forStep : Lean.Syntax × Option Lean.Syntax × Lean.Syntax → m Unit) : Steps → m Unit
  | .done _ => pure ()
  | .cons e1 why (.done e2) => forStep (e1, why, e2)
  | .cons e1 why (.cons e2 why2 more) => do
    forStep (e1, why, e2)
    process forStep (.cons e2 why2 more)

partial def getSteps : Lean.Syntax → Lean.Elab.Command.CommandElabM Steps
  | `(eqSteps|$t:term) => pure (.done t)
  | `(eqSteps|$t:term ={ }= $more:eqSteps) => do
    return (.cons t none (← getSteps more))
  | `(eqSteps|$t:term ={ $why:term }= $more:eqSteps) => do
    return (.cons t (some why) (← getSteps more))
  | other => throwError "Invalid equational steps {other}"

elab_rules : command
  | `(equational steps {{{ $name }}} $stepStx:eqSteps stop equational steps) =>
    open Lean.Elab.Command in
    open Lean.Elab.Term in
    open Lean in
    open Lean.Meta in do
      let exprs ← getSteps stepStx
      if let .done e := exprs then liftTermElabM <| withDeclName name.raw.getId do
        let _ ← elabTerm e none
      exprs.process fun
        | (e1, why, e2) =>
          liftTermElabM <| withDeclName name.raw.getId do
            let x ← elabTerm e1 none
            let y ← elabTerm e2 none
            synthesizeSyntheticMVarsNoPostponing
            match why with
            | none =>
              unless (← isDefEq x y) do
                throwError "Example equational step {y} ===> {x} is incorrect\n----------\n\t {(← whnf y)}\n ≠\n\t {(← whnf x)}\n----------\n\t {(← reduceAll y)}\n ≠\n\t {(← reduceAll x)}"
            | some p =>
              let e1' : TSyntax `term := ⟨e1⟩
              let e2' : TSyntax `term := ⟨e2⟩
              let eq ← elabTermEnsuringType (← `($e1' = $e2')) (some (mkSort Level.zero))
              let _ ← elabTermEnsuringType p (some eq)
              synthesizeSyntheticMVarsNoPostponing

[Patrick Massot]

Thanks for the detailed explanations! I think it doesn't make much sense to have a chapter on proofs per se. There is already Theorem proving in Lean for that (and we'll port Mathematics in Lean at some point). It would be much more consistent to cover proofs for programming such as termination proofs. I guess that proofs of programs would need a lot more space, maybe a different book.

[Patrick Massot]

Stuff about lake and ffi would be a nice continuation but I understand that funding is running out, and the current plan is already a full self-contained book.

[Mario Carneiro]

I think proofs need to be covered at some level, if only to inform readers that there's a whole other book to read if that's your interest

[Mario Carneiro]

ideally there should be some light proof examples for the kinds of proofs that come up in programming applications, like termination proofs and using the a[i] array indexing operator

[Mario Carneiro]

I think teaching it as two separate languages sends the wrong message

[Patrick Massot]

Yes, David wrote he's thinking about covering termination proofs.

[Arien Malec]

Another lens might be proving things that would be unit tests in other languages, as well as designing an API surface area that's amenable to proof.

[Arien Malec]

The canonical killer app for dependently typed languages is the "typestate pattern" - e.g., a auth component that provably can't be in the wrong state

[James Gallicchio]

Arien Malec said:

Another lens might be proving things that would be unit tests in other languages, as well as designing an API surface area that's amenable to proof.

my impression was both these things are still major research areas, no? :grimacing:

[Mario Carneiro]

examples with Connection (open : Bool) : Type and such are cute but honestly not that relevant to programming in lean and don't really sell the language when something like haskell is the point of comparison

[Mario Carneiro]

more interesting stuff would be a type which only holds prime numbers, or an acyclic graph structure

[Arien Malec]

I come from a Rust perspective & this article was highly influential...

https://docs.idris-lang.org/en/latest/st/machines.html

[Mario Carneiro]

You can't even really do the Connection thing very well because lean doesn't have linear types

[Mario Carneiro]

which is what you actually need to make that example work

[Arien Malec]

E.g., http://cliffle.com/blog/rust-typestate/

[Mario Carneiro]

and it doesn't play well with monads either

[Arien Malec]

huh...

[Mario Carneiro]

that idris example can't be done in lean directly because the do notation doesn't have typestate like that

[Arien Malec]

then yeah, a dag example would be useful...

[Paul Chisholm]

@David Thrane Christiansen
Assorted minor comments on the first 4 chapters. Many are stylistic in nature so just ignore if you don't agree.

1.3 Defining Functions

• 3rd para: remove second instance of just.
• 6th para: Remove s from As a special cases.
• last para (before exercise): drop actually in 1st line.

1.4 Defining Type/Messages You May Meet

• 1st para: it says ...by a feature of Lean that has not yet been introduced; at this point the reader has no clue what that feature is or why it matters. Perhaps a forward reference would clarify.
• Despite the title of the section, it doesn't seem to be primarily about the messages.
• It should be an h2 heading so it isn't inside Defining Types. All other Messages... subsections are at the h2 level.

1.4 Structures

• Para starting The typical way: a instance should be an instance.
• Same para: delete the first occurrence of both.

1.4 Behind the Scenes

• Para starting Constructors have...: delete first occurrence of that.

1.5 Datatypes and Patterns

• In the third para you say most user defined datatypes are inductive datatypes. If you mean that in the general sense, so that structure definitions are included, then I agree. If you specifically mean types that are recursively defined, then I would argue most are structure definitions.
• Para starting This definition has...: the 5th sentence seems to be a bit overloaded with name - could it be reworded?

1.6 Polymorphism

• Para starting In this example...: two occurrences of because reads a little clumsy.
• Last para: would pattern-matches to run the same pattern be better expressed as pattern-matches against the same pattern?
• Last para: a couple of #check/eval lines after the definition of posOrNegThree would be useful to clarify what is happening.

1.6 Implicit Arguments

• Para starting In the standard library...: delete the first that.

1.6 Option

• Note in the definition of Option the decoration : Type has been added just before the where, and this appears consistently in all subsequent definitions. All prior type definitions omit it.
• Where you have #eval [].head? (α := Int), might note that #eval ([]:List Int).head? is also possible?

1.6 Prod

• Where you note using domain terminology can make it easier to read the code, might also add specific structures help to avoid errors.

1.7 Local Definitions

• Consider giving an alternate definition of helper using where (which interestingly doesn't require rec).

1.7 Anonymous Functions

• Consider using \mapsto instead of =>, though that is compromised since \mapsto can't be used in patterns.
• The centred dot is \. or \centerdot, not \cdot.

2.3 Lakefiles

• Since the standard library std4 has now been separated from core, and is likely to be required for many packages, it would be good to show how std4 is included

require std from git "https://github.com/leanprover/std4" @ "main"

2.4 Getting Started

• For consistency with 2.3, it would be preferable to include the guillemets.

2.6 do Notation

• Should and given a unique name be gives them a unique name?

3 Indexing Without Evidence

• 1st para: an question -> a question.
• Is the example #eval woodlandCritters[1]! supposed to show a crash? Is the index supposed to be out of bounds?

3 Exercises

• exercise 1, rfl not sufficient for 5 < 18.

4.1 Classes and Instances

• Someone following along and entering the examples may be a bit confused when they enter #eval Plus.plus 5 3 and get an error rather than 8 as shown. Not till later is it explained.

4.1 Conversion to Strings

• In definition of posToString possibly have s!"({s})" for consistency. You perhaps avoided this as the two ss might confuse?

4.1 Exercises

• To this point the exercises have been small, then we get HTTP, which is much bigger and requires background information. Subsequent exercises go back to being small again. It is certainly an interesting exercise, but perhaps a bit of a leap.

4.4 Arrays

• Para starting In pure functional...: contain an optimizations -> contain an optimization or contain optimizations.

4.4 Non-Empty Lists

• Para starting This fact can be...: delete second instance of that.
• In definition of NonEmptyList.get, replace ok with _.

4.5 Equality and Ordering

• Having defined Pos as an instance of Ord, could add something like

instance : LT Pos where
  lt x y := compare x y == Ordering.lt

#eval (1 : Pos) < (2 : Pos)

Possibly even

instance : LE Pos where
  le x y := compare x y != Ordering.gt

#eval (1 : Pos) ≤ (2 : Pos)

and explain why the #eval throws an error, though

#eval (1 : Pos) < (2 : Pos) || (1 : Pos) == (2 : Pos)

succeeds.

4.5 Deriving Standard Classes

• In one of the Messages sections might be worth mention that deriving sometimes throws messages like this:

default handlers have not been implemented yet, class: 'ToString' types: [X]

which suggests deriving may be possible in future for that class.

4.5 Functors

• Possibly note (· + 5) <$> [1, 2, 3] can also be written [1, 2, 3].map (· + 5).

4.6 Chaining Coercions

• Follow the definition of coercedToB with #eval coercedToB to demonstrate it is B.b (though that means you would need deriving Repr on B).
• Para starting Some coercions...: contains in in.

4.6 Coercing to Functions

• 1st para: there are more than one way -> there is more than one way.

4.6 Aside: JSON as a String

• Para starting The function that emits...: delete second that in is complicated enough that Lean cannot see that the recursive calls....

4.7 Examples

• The sentence Examples may create define functions by accepting arguments:; did you intend both create and define here?

[David Thrane Christiansen]

@Paul Chisholm Thank you for your careful attention and helpful comments! I won't have time to work on the book for a bit due to FOSDEM, but I'll be sure to look over everything when I'm able.

[Arthur Paulino]

Hi! I have a suggestion for a topic: threads. Doing IO tasks in threads, sharing/locking data, joining etc.

I am a complete noob in the subject and it would be lovely to learn about those in Lean 4. What do you guys think?

[David Thrane Christiansen]

That would indeed be a good topic! However, the scope of this book is fixed, and there's no more time for additional topics. I'm really trying to get the parts through that are conceptually different from imperative programming, not comprehensively document the language and tools. Perhaps a thread chapter would be better suited to the manual?

[Wojciech Nawrocki]

Mario Carneiro said:

You can't even really do the Connection thing very well because lean doesn't have linear types

The linked ST example is from Idris 1 which doesn't have linear types either

[Wojciech Nawrocki]

Arien Malec said:

then yeah, a dag example would be useful...

FWIW I have just started working on this. The code is super specific to the project it's for, but if it ends up working well it could be extracted out into its own library or std4 or somewhere.

[Arien Malec]

Super cool example!

[Arien Malec]

James Gallicchio said:

Arien Malec said:

Another lens might be proving things that would be unit tests in other languages, as well as designing an API surface area that's amenable to proof.

my impression was both these things are still major research areas, no? :grimacing:

My impression is that proving all things that would be unit tests in other languages feels hard but proving some things that would be unit tests n other languages is a superpower of a language like Lean, where the proof language and the programming language are the same thing. E.g., LawfulFoo, or more practically something that would absolutely be part of the test suite: docs4#List.replicate_zero docs4#List.eq_replicate

[David Thrane Christiansen]

Hello everyone! There's a new release of the book out, with a chapter on programming with dependent types.

Thank you very much for the excellent feedback and careful reading so far. There's one more chapter to go!

https://leanprover.github.io/functional_programming_in_lean/

[Malcolm Langfield]

Not sure if this is still the place to submit errata, but there is a typo in the last paragraph of the introduction to Chapter 8:

Expressive specifications can be complicated to fulfill, and there is a real risk of creating tying oneself in knots and being unable to complete the program.

Probably "creating" should not be there?

[David Thrane Christiansen]

Malcolm Langfield said:

Not sure if this is still the place to submit errata, but there is a typo in the last paragraph of the introduction to Chapter 8:

Expressive specifications can be complicated to fulfill, and there is a real risk of creating tying oneself in knots and being unable to complete the program.

Probably "creating" should not be there?

This is still a good place - I just don't know how to get Zulip to notify me about posts to threads, and I missed this until now. It's fixed!

[David Thrane Christiansen]

@Paul Chisholm Thank you again for those thorough comments - they're all integrated in the latest development version of the book. I'm sorry it took me a while to get to them.