Functional Programming in Lean

Stream: lean4

[Henrik Böving]

What are the plans for https://github.com/leanprover/functional_programming_in_lean, can the community reasonably help?

[Leonardo de Moura]

It is a public repo that we are going to use to deploy the book that @David Thrane Christiansen is writing.
We plan to release the chapters incrementally. We hope to release the first chapter soon, and comments and feedback will be very welcome.

[Leonardo de Moura]

@Henrik Böving BTW, I am very grateful for all the work you, Arthur, and others are putting in the Metaprogramming book.

[Rosie Baish]

Leonardo de Moura said:

[C]omments and feedback will be very welcome.

What's the preferred method of doing this?
I had a dig around and couldn't find the source repo anywhere, should I just type up notes as an issue in the gh_pages repo?

[Leonardo de Moura]

@Rosie Baish Great questions. The book repo is currently private, but we will make it public in the future.
Regarding feedback, you can post it here or contact David directly. He has already shared his email: david@davidchristiansen.dk.

[David Thrane Christiansen]

Hi! Email is great, as is contacting me here. If you PM or mention me, I get a notification.

The source of the book is not presently public because I have fairly limited time to work on it, and public repositories require maintenance, moderation, and curation that would take more time away from writing.

[Nicolas Rouquette]

There is an interesting discussion about OO polymorphism that involve structures. I noticed that none of the 3 books on Lean explains the generation of "to<Parent>" structural slicing methods and that these methods do not correspond to OO-style upcasts.

[Jeremy Salwen]

@David Thrane Christiansen Thanks for the great book! I think I spotted an error in the Monad introduction. You are calling "pre-order numbering" what looks to me to be a post-order numbering, at least according to the terminology on wikipedia: https://en.wikipedia.org/wiki/Tree_traversal (i.e. visiting left child, right child, and then the node, in that order). https://leanprover.github.io/functional_programming_in_lean/monads.html#numbering-tree-nodes

[Mario Carneiro]

Actually it looks like an inorder traversal (left child, then the root, then the right child)

[David Thrane Christiansen]

Yep, it's inorder. Those names...

I'll fix it. Thanks!

[Jeremy Salwen]

"This is because the nodes in the right subtree should be numbered starting from the highest number assigned in the left subtree" I think this should be "one after the highest" or something, since the next number will be the root, then the right subtree.

[David Thrane Christiansen]

Jeremy Salwen said:

"This is because the nodes in the right subtree should be numbered starting from the highest number assigned in the left subtree" I think this should be "one after the highest" or something, since the next number will be the root, then the right subtree.

Thanks! Fixed in the latest development version.

[Patrick Massot]

@David Thrane Christiansen I began to read the new chapter and I'm not sure I'm convinced by the running example in https://leanprover.github.io/functional_programming_in_lean/dependent-types/universe-pattern.html. The "Type Classes vs Universes" section explains when universes à la Tarski can be better than type classes but then it seems to me that your example would be perfectly handled by the decidable type class. For instance, using docs4#Fintype.decidablePiFintype from mathlib4, we can write:

import Mathlib.Data.Fintype.Basic

#eval decide ((fun _ => true : Bool → Bool) = (fun b => b == b))

#eval decide ((fun _ => true : Bool → Bool) = not)

[Mac Malone]

@David Thrane Christiansen One slight clarification I noticed while skimming the book. In 2.3, you mention that open Lake DSL opens the namespaces Lake and DSL. More specifically, it opens Lake and Lake.DSL.

[Eric Wieser]

That's a little surprising, given that's not what it means in mathlib3. Does mathport translate open foo bar to open foo open bar?

[Arthur Paulino]

How does it work in mathlib3?

[Eric Wieser]

open foo bar means open foo open bar in lean 3

[Henrik Böving]

This is also what Lean 4 does. But for example with Lake.DSL if you open Lake the Lake namespace is already open so naturally DSL is now a top level namespace and if you open DSL you open that top level namespace which ends up opening Lake.DSL

[Kevin Buzzard]

So the (fairly common in category theory) mathlib3 idiom open category_theory category_theory.limits can now be open CategoryTheory Limits in lean 4 by the sounds of things.

[Henrik Böving]

yes

[Newell Jensen]

@David Thrane Christiansen in Datatypes and Patterns section you have "a similar definition of definition of Bool"

[Newell Jensen]

Also "if the numerator is less that the divisor" (that --> than)

[Bulhwi Cha]

@David Thrane Christiansen In Section Datatypes and Patterns, I think n < k in the following code should be k = 0 ∨ n < k. Otherwise, it'd be hard to prove termination for div.

def div (n : Nat) (k : Nat) : Nat :=
  if n < k then
    0
  else Nat.succ (div (n - k) k)

[Bulhwi Cha]

Here's the proof of termination for div:

import Std.Data.Nat.Lemmas

theorem div_rec_lemma {x y : Nat} : ¬(k = 0 ∨ n < k) → n - k < n := by
  intro h
  have h₁ : k ≠ 0 ∧ ¬ n < k := by rw [not_or] at h; assumption
  have h₂ : 0 < k ∧ k ≤ n := by
    constructor
    · exact Nat.zero_lt_of_ne_zero h₁.left
    · exact Nat.le_of_not_lt h₁.right
  apply Nat.div_rec_lemma
  assumption

def div (n k : Nat) : Nat :=
  if k = 0 ∨ n < k then
    0
  else Nat.succ (div (n - k) k)
decreasing_by show n - k < n; apply div_rec_lemma <;> assumption

[David Thrane Christiansen]

Your suggestion provides an incorrect answer for k = 0, for which division is undefined, not 0 :-)

In the imminently-released final chapter, there's also a proof of termination, and the section in question links to it. I'll be interested to hear what you think!

[David Thrane Christiansen]

(and thank you for the careful attention)

[David Thrane Christiansen]

Newell Jensen said:

David Thrane Christiansen in Datatypes and Patterns section you have "a similar definition of definition of Bool"

Thanks! Fixed in the imminent release :-)

[David Thrane Christiansen]

Mac said:

David Thrane Christiansen One slight clarification I noticed while skimming the book. In 2.3, you mention that open Lake DSL opens the namespaces Lake and DSL. More specifically, it opens Lake and Lake.DSL.

Thank you! This is a good clarification.

[Kevin Buzzard]

In Lean, division by 0 is defined and equal to 0.

[David Thrane Christiansen]

This is a reasonable pragmatic thing to do as part of a standard library, but I don't think it's a good way to make the point that I want to make about recursive functions

[David Thrane Christiansen]

Though that is also probably worth a little note here :-)

[Kevin Buzzard]

I'm happy if you don't want your division by 0 to be a junk value. But I think the point Bulhwi is making is that your claim "This program terminates for all inputs" just after the definition of div is not correct, because your code really doesn't terminate if k=0.

[David Thrane Christiansen]

Oh, absolutely! That's definitely the case (and fixed now)

[Bulhwi Cha]

According to the constructors, a List α can be built with either nil or cons. The constructor nil represents empty lists, and the constructor cons represents a single element in the linked list.

In Section Polymorphism, I'm not sure how I should understand the clause "the constructor cons represents a single element in the linked list." Looking at the Wikipedia page on lists, it seems the following explanation makes more sense:

the constructor cons represents an operation that adds an element at the beginning of another list.

[David Thrane Christiansen]

Thanks, I can see how that's confusing! It's important to the writing style in use here that constructors are not verbs - they're inert and don't compute. But I'll adjust it!

[David Thrane Christiansen]

Well, the final prerelease of the book prior to my deadline at the end of the month is up. Thank you all for your feedback so far, and I'll be spending the rest of the time polishing and fixing mistakes: https://leanprover.github.io/functional_programming_in_lean/

[Mario Carneiro]

David Thrane Christiansen said:

Thanks, I can see how that's confusing! It's important to the writing style in use here that constructors are not verbs - they're inert and don't compute. But I'll adjust it!

Phrasing the distinction grammatically like this might be a problem if people notice that the default constructor for a structure is called mk which is an abbreviation of "make" which is a verb

[David Thrane Christiansen]

It's more that in the earlier chapters, I think it's very important to distinguish what the word "constructor" means in something like Lean vs what it means in something like Java or Python. This is far from the only way the information is conveyed, but redundancy and consistency are part of making texts that confuse people less.

[Bulhwi Cha]

Current documentation in Section Additional Conveniences:

The first step is to move the arguments' types to the right of the definition's type, in the form of a function type.

Suggestion:

The first step is to move the arguments' types to the right of the colon, in the form of a function type.

[Bulhwi Cha]

It might be worth mentioning in Section Additional Conveniences that we can also use the Unicode symbol ↦ to create an anonymous function.

[Evante Garza]

Functional Programming in Lean may be interesting to readers who enjoy jokes about recursion.

This made me laugh, thanks for a great book!

[David Thrane Christiansen]

Bulhwi Cha said:

Current documentation in Section Additional Conveniences:

The first step is to move the arguments' types to the right of the definition's type, in the form of a function type.

Suggestion:

The first step is to move the arguments' types to the right of the colon, in the form of a function type.

This is a nice improvement - thanks!

[David Thrane Christiansen]

Bulhwi Cha said:

It might be worth mentioning in Section Additional Conveniences that we can also use the Unicode symbol ↦ to create an anonymous function.

I haven't seen that notation in enough Lean code to think that it's essential knowledge at this early stage, and I feel like this section already has enough syntactic variations! It doesn't provide any practical differences from the fun notation, does it?

[Henrik Böving]

No it was mostly introduced because the mathematicians kept asking us for it

[Jireh Loreaux]

The more good notation the better. I've been tempted to use things like α →+* β in my courses otherwise unrelated to Lean. Out of curiosity, does anyone else do this?

[Patrick Massot]

I'm pretty sure I've used α → β. And I discuss math with Anatole on the blackboard we both use Lean notations.

[Mario Carneiro]

um, are you saying that you used functions?

[Mario Carneiro]

I mean that's not really a lean patented invention

[Henrik Böving]

I think he might be saying that he used \rightarrow instead of \mapsto to denote that something is a function?

[Mario Carneiro]

you wouldn't use mapsto in that position

[Mario Carneiro]

mapsto in maths means fun not →

[Adam Topaz]

I assume Patrick means writing $\alpha \to \beta$ instead of $Fun(\alpha,\beta)$ for the collection of all functions.

[Adam Topaz]

In math we would (unfortunately!) never write something like $f : \alpha \to \beta \to \gamma$, for example.

[Patrick Massot]

Yes, we certainly write $f : α → β$, but never $α → β$ alone.

[Patrick Massot]

And of course we never write $α → β → γ$ with its Lean meaning.

[Moritz Doll]

Jireh Loreaux said:

The more good notation the better. I've been tempted to use things like α →+* β in my courses otherwise unrelated to Lean. Out of curiosity, does anyone else do this?

not in courses or anything, but I use α →ₗ β for linear functions on the blackboard

[David Thrane Christiansen]

Jireh Loreaux said:

The more good notation the better.

I think that this is not true for the first chapter of introductory material. The goal of that chapter is to help readers get up to speed with the basic patterns of thought and the most common syntax, building a platform for the more challenging ideas that come later. In fact, I think that Chapter 1 should have as little notation as possible, while still enabling the rest of the book to be written, because unfamiliar syntax is a common stumbling block.

[Yaël Dillies]

I personally started writing $\alpha \underset{\mathit{properties}}\longrightarrow \beta$ in my notes, because it's much easier to decypher six months later than the obnoxious collection of symbols mathematicians came up with.

[Johan Commelin]

Category theorists have been writing $C(X, Y)$ for the set (space) of morphisms from $X$ to $Y$ in the category $C$. Maybe mostly useful if $C$ is a rather short name.

[Scott Morrison]

I even write $C(X → Y)$.

[Yaël Dillies]

EDIT: Sorry David, I accidentally read the wrong book.

I think it's worth mentioning in Induction and Recursion that definitional equalities in recursive/multiple arguments pattern matches are only guaranteed once all pattern-matched variables have been destructed. This is a common gotcha for beginners.

[Yaël Dillies]

I don't have an example at hand, but the reason is that Lean adds pattern-matches within the definition and the cases can be split quite unexpectedly.

[Yaël Dillies]

I also see a typo in this same section: defaulty should be default.

[Mario Carneiro]

I think that is a bit of a technical point and likely would not come up on examples in the context of the book. I'm not even sure the over-matching bug is an issue to the same extent as it was in lean 3, and I don't think it represents an intrinsic truth in any case (i.e. it could potentially be true or not depending on details of the compiler that might change in future versions), which would make it a poor choice to put in a book which is intended to last.

[Yaël Dillies]

A few other things:

• propostion → proposition
• The section Local Recursive Declarations is duplicated

[Yaël Dillies]

For Type Classes

• "Instances which are declared last are tried first". I thought that wasn't true anymore?
• "Moreover, if instances are declared in other modules, the order in which they are tried depends on the order in which namespaces are opened.". Is this about modules, or about namespaces? Why would there be a relation between both?

[Jireh Loreaux]

@David Thrane Christiansen: agreed, not introducing a ton of notation up front is important for readability and comprehension. I was just responding to this:
Henrik Böving said:

No ↦ was mostly introduced because the mathematicians kept asking us for it

[Yaël Dillies]

In Axioms and Computation:

• You seem to have a broken reference: :numref:choice
• extenionality → extensionality
• I don't know whether that is on purpose but I would expect theorem inhabited_of_nonempty :Nonempty α → Inhabited α to instead be a noncomputable def, since Inhabited is data.
• "In contrast to p ∨ ¬ p, which can only eliminate to Prop, the type decidable p is equivalent to the sum type Sum p (¬ p)". It should be Decidable p, and PSum p (¬ p) (Sum only accepts Type, not Prop)

[Yaël Dillies]

Wait, sorry, I accidentally went on to read TPIL instead of your book :scream:

[Patrick Massot]

Yaël, I think you should edit your messages to avoid confusing David when he'll read that discussion.

[Mario Carneiro]

Yaël Dillies said:

For Type Classes

• "Instances which are declared last are tried first". I thought that wasn't true anymore?

It is still true, but being tried first means less than it used to because there is a filter in front that does the majority of the selection work, meaning that it is rare to have multiple options to choose from in the first place

[Mario Carneiro]

Yaël Dillies said:

• "Moreover, if instances are declared in other modules, the order in which they are tried depends on the order in which namespaces are opened.". Is this about modules, or about namespaces? Why would there be a relation between both?

This sounds like a typo, it should say "the order in which modules are imported". Opening namespaces does nothing to instance search (except for making scoped instances available)

[David Thrane Christiansen]

Jireh Loreaux said:

David Thrane Christiansen: agreed, not introducing a ton of notation up front is important for readability and comprehension ...

Sometimes, the lack of threading in Zulip is confusing :-)

[David Thrane Christiansen]

@Yaël Dillies I must admit I spent a bit of time confusedly grepping for what you found here! Thanks for the edit and update.

[Zhiyuan Bao]

@David Thrane Christiansen Thanks for your great book! Currently reading it and learned a lot!
I think I find a typo in the last release of this book. At 2.1 Running a program, subsection Anatomy of a Greeting, last sentence of first paragraph, it says: "Instead of a being a function that has side effects, main consists of a description of effects to be carried out." The first 'a' seems redundant, maybe it should be "Instead of being a function that ..."

[David Thrane Christiansen]

Zhiyuan Bao said:

David Thrane Christiansen Thanks for your great book! Currently reading it and learned a lot!
I think I find a typo in the last release of this book. At 2.1 Running a program, subsection Anatomy of a Greeting, last sentence of first paragraph, it says: "Instead of a being a function that has side effects, main consists of a description of effects to be carried out." The first 'a' seems redundant, maybe it should be "Instead of being a function that ..."

Thanks! I just fixed it in the repo, and it will be in the imminent final release.

[Bulhwi Cha]

Current documentation in Section Real-World Functional Programming:

After all, the entire universe cannot be turned in to a Lean value and placed into memory.

Suggestion: "turned in to" → "turned into"

[David Thrane Christiansen]

Thanks! Fixed.

[Bulhwi Cha]

Current documentation in Section Combining IO Actions:

IO.getStdin and IO.getStdout are IO actions in order to allow stdin and stdout to be locally overridden in a program, which can be convenient.

Suggestion: "in order to allow" → "that allow"

[David Thrane Christiansen]

Bulhwi Cha said:

Suggestion: "in order to allow" → "that allow"

This would change the meaning. Because they are IO actions, rather than global bindings, they can be overridden. But the IO actions themselves do not allow this override to take place.

Thanks for the careful reading!

[Bulhwi Cha]

The last sentence of Section Handling Input:

Thus, process does not introduce any non-termination itself.

Suggestion: "non-termination itself" → "non-termination of itself"

I'm not sure whether it's necessary to put "of" between "non-termination" and "itself."

[Mario Carneiro]

I don't think that is grammatical

[Kyle Miller]

It might be clearer as "Thus, process does not itself introduce any non-termination." You could perhaps insert "in", but inserting an "of" would be wrong.

[David Thrane Christiansen]

I got rid of "itself", which I think is more clear and fits the meaning that was intended. Thanks!

[Bernhard Reinke]

@David Thrane Christiansen Thanks for the great book! I have a question for the exercise of 6.4 Alternatives:

I worked through the section and also proved that the definition of Validate ε using nonempty lists satisfies the laws of an applicative functor. I am not so sure whether this still holds for the version of the exercise with TreeError. In particular, append is not associative for TreeError, so seq shouldn't be associative for the case of composing 3 errors.

Could you include the path information by still using nonempty lists in the definition of Validate, and using Validate (List String × Field × String)instead of Validate (Field × String), where the first factor includes the path information of an error?

[David Thrane Christiansen]

You're right - this is a bad exercise for this reason. I've created an issue so I remember to fix it: https://github.com/leanprover/fp-lean/issues/124

I'm really busy right now but I hope to have time in the not-too-distant future to take care of this kind of thing. Thank you for letting me know!