4 ms·

Functional Programming in Lean

159 points by d_christiansen 3y ago

dharmatech 3y ago
Demo of Lean I recorded a few years back: https://youtu.be/p4IrbnPomXg https://youtu.be/p4IrbnPomXg
d_christiansen 3y ago
Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.
- mdm12 3y ago
  Congratulations on the publication! As a dabbler in strictly typed functional programming languages like Scala and F#, I have always been curious about proof-oriented languages such as Coq or Agda, but found it difficult to justify the time investment. Lean seems to position itself as a theorem proving language that also supports general-purpose programs. Looking forward to digging into your book!
  - epgui 3y ago
    Agda and Idris both also position themselves similarly.
    - siknad 3y ago
      Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
      - epgui 3y ago
        You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).
  - d_christiansen 3y ago
    Thanks! I hope you find it valuable! Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.
- ykonstant 3y ago
  Thank you very much for this book. It has been invaluable for my introduction to Lean and a joy to study from. I still have not read the last chapter, looking forward to it! Kudos for your effort, and I hope you will write some more stuff about Lean in the future.
  - d_christiansen 3y ago
    Thank you for reading it, and I hope that the final chapter is also enjoyable for you. Right now, I plan to take a break - this book occupied every Saturday for about a year, and some time off is in order. But Lean is tons of fun, and I'd like to get back into it once I'm recovered a bit.
- deleted 3y ago
  [deleted]
- Reitet00 3y ago
  This looks very nice! Is epub version planned?
  - d_christiansen 3y ago
    Unfortunately not. I wanted to produce PDF and epub versions in parallel with the HTML version, but getting those to be of sufficient quality would have blown the time budget for the project. There's some old code in the Git history for dumping the source to Pandoc's dialect of Markdown, from which I was going to generate those, but the differences in Markdown dialects are enough that it was a fair bit of work. Dropping a print version and focusing on epub could very well be faster, as I suspect that an mdbook->epub pipeline is less challenging than creating a quality print-ready PDF. But no plans right now.
- pjmlp 3y ago
  Congratulations on releasing it. Looking forward to read it during Summer time.
doogah 3y ago
[dead]
ggm 3y ago
Minor thing. Purely as a side: in C and C++, the conditional statement is written using if and else, while the conditional expression is written with a ternary operator ? and :. ending a sentence with . is a must. Including a period directly after a syntactic construct about ? and : is .. jarring because it is possible to attempt to read this as :. as an atomic construct in the language. Or even worse, the three-dots pyramid in some mathematical proof notations.
- AdieuToLogic 3y ago
  > Also, I always find it interesting the ternary operation is constructed in statements/expressions in ? ... : notation but actually has "two" operators there. the ? is the conditional, the : is the binary-choice. It's a language syntax choice which "side" is true or false and it is also true that you can't construct statements in : without a prior ? but .. its hardly a single operator in syntax terms if it has two disjoint components. := is an unambiguous single operation. condition ? x : y is ... not. It's definedly ambiguous! In C++, the lexical construct you describe is an atomic operator[0] and neither an expression nor a statement: The first operand of the conditional operator is evaluated and contextually converted to bool. After both the value evaluation and all side effects of the first operand are completed, if the result was true, the second operand is evaluated. If the result was false, the third operand is evaluated. 0 - https://en.cppreference.com/w/cpp/language/operator_other https://en.cppreference.com/w/cpp/language/operator_other
  - ggm 3y ago
    I took my comments about ?...: notation out. Basically, at a syntactic level its tempting to regard ? as "the operator" and : as some other operator but really the ternary operation only exists as some hypothetical function in 3 arguments: ternary(condition, true-path, false-path) which executes either true-path or false-path depending on condition. But in notational terms, how "big" condition and true and false parts are is rather unconstrained, so you wind up with the ? and the : widely separated. They aren't operators in the higher sense: they're the syntax which forms the ternary operation as a whole over the expression and it's condition. Lexing bleeds into syntax and syntax bleeds into semantics. :. is a possible faux-pas in lexing the sentence around the ?...: construct because of :. being unfortunate.
foderking 3y ago
this is actually a good read
- d_christiansen 3y ago
  Thank you! I hope you enjoy the rest of it.
revskill 3y ago
Is this production ready ? How about performance (comparison with Rust)
- siknad 3y ago
  Lean is currently moving to the 4th iteration which is the first intended to be a general-purpose programming language. It "is currently being released as milestone releases towards a first stable release". For now the main goal is to port mathlib to the new version, and then they will concentrate on the compiler. So it is not production ready. But that doesn't mean it is not suitable for building any programs now. There is a simple raytracer written in Lean [1]. I have built a chip8 interpreter with it and the only problem was the lack of an ecosystem, meaning I had to build the necessary libraries myself. Now it has a RC GC and boxes everything >= 64 bits (including struct fields and IO/ST results), and as the compiler isn't polished it is probably significantly slower. In the referenced raytracer repo you can find rendering time compared to the C implementation (Lean is 25x slower, but that was a year ago). [1] https://github.com/kmill/lean4-raytracer https://github.com/kmill/lean4-raytracer
- reuben364 3y ago
  While Lean4 is meant to be much more of a general purpose language than it's predecessor, it is still built with being a proof assistant in mind. That being said it is self hosted and has been in development and use for quite some time, which says something of it's readiness. Tooling around it great (it is installed with a rustup fork called elan). As far as performance, it uses a particular version of ref-counting that allows mutation of unique references based on run-time tracking rather than compile time. If you accidentally keep a reference to an array and modify it, then you end up copying it rather than just mutating it.
theresistor 3y ago
I'm interested to know why I would want to learn Lean if I'm already familiar with Idris.
- siknad 3y ago
  Big: * tactics (proof scripts are a lot easier than manual proving) * syntax extensibility (Racket-like, supports custom elaboration/delaboration) * mathlib (library of formalized math) * tooling (can't say it's better, I haven't used Idris, but it's at least a lot nicer than Agda's: rustup-like version manager `elan`, own build system `lake`, official vscode extension supporting mini web apps which can interact with the code) Small things I can remember: * do-notation with early return and imperative loops * easier termination proof handling (provide some expression using function arguments with `decreasing_by` and prove it's decreasing with `termination_by` block, which may be automatic even for non-structural recursion because of some built-in tactic)
  - dmytrish 3y ago
    Regarding tactics: I started with Coq and I felt for a long time that I had no idea what tactics actually do. Proofs with tactics look nice on the surface, but I really did not like hidden state and hidden actions. Redoing some proofs in Lean by construction of proof terms was eye-opening, it's just functional programming with dependent types! I still think that teaching with tactics first without exposing proof terms is a mistake. I've learned to see the value of tactics later, again thanks to Lean: there are proofs that are more natural in the tactics style. Sometimes a mixed approach is ideal: growing intermediate proof terms from the premises and then wrangling the hypothesis with tactics to meet the lemmas.
- d_christiansen 3y ago
  Lean occupies a different point in the design space. Its type theory is simpler and more conservative, its metaprogramming system is more reminiscent of Racket's (including hygienic procedural macros), and the focus on supporting professional mathematicians gives a different feel to the community and libraries. I think both are worth knowing, but either is great to learn. I hope the two projects learn more from each other in the future.
calrizien 3y ago
Is there a public compendium of lean proofs? More specifically, has Euclid's Elements been translated into lean?
- arlort 3y ago
  Is this what you're looking for? https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib
- dmytrish 3y ago
  There's Mathlib: https://leanprover-community.github.io/mathlib_docs/index.html https://leanprover-community.github.io/mathlib_docs/index.ht... I was stunned when I discovered it, because it does exactly what its name suggests: it's a huge library of math proofs available as a library in Lean.
sullyj3 3y ago
Does lean have an analogue to hoogle?
- fogof 3y ago
  For searching using search terms for theorems in mathlib, there is the mathlib documentation page (for Lean 3 https://leanprover-community.github.io/mathlib_docs/ https://leanprover-community.github.io/mathlib_docs/ and Lean 4 https://leanprover-community.github.io/mathlib4_docs/ https://leanprover-community.github.io/mathlib4_docs/). To find theorems by type, I find the best way is to use the `library_search` tactic from inside Lean itself.

Demo of Lean I recorded a few years back: https://youtu.be/p4IrbnPomXg https://youtu.be/p4IrbnPomXg

Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.

mdm12 3y ago
Congratulations on the publication! As a dabbler in strictly typed functional programming languages like Scala and F#, I have always been curious about proof-oriented languages such as Coq or Agda, but found it difficult to justify the time investment. Lean seems to position itself as a theorem proving language that also supports general-purpose programs. Looking forward to digging into your book!
- epgui 3y ago
  Agda and Idris both also position themselves similarly.
  - siknad 3y ago
    Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
    - epgui 3y ago
      You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).
- d_christiansen 3y ago
  Thanks! I hope you find it valuable! Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.
ykonstant 3y ago
Thank you very much for this book. It has been invaluable for my introduction to Lean and a joy to study from. I still have not read the last chapter, looking forward to it! Kudos for your effort, and I hope you will write some more stuff about Lean in the future.
- d_christiansen 3y ago
  Thank you for reading it, and I hope that the final chapter is also enjoyable for you. Right now, I plan to take a break - this book occupied every Saturday for about a year, and some time off is in order. But Lean is tons of fun, and I'd like to get back into it once I'm recovered a bit.
deleted 3y ago
[deleted]
Reitet00 3y ago
This looks very nice! Is epub version planned?
- d_christiansen 3y ago
  Unfortunately not. I wanted to produce PDF and epub versions in parallel with the HTML version, but getting those to be of sufficient quality would have blown the time budget for the project. There's some old code in the Git history for dumping the source to Pandoc's dialect of Markdown, from which I was going to generate those, but the differences in Markdown dialects are enough that it was a fair bit of work. Dropping a print version and focusing on epub could very well be faster, as I suspect that an mdbook->epub pipeline is less challenging than creating a quality print-ready PDF. But no plans right now.
pjmlp 3y ago
Congratulations on releasing it. Looking forward to read it during Summer time.

doogah 3y ago

[dead]

ggm 3y ago

Minor thing. Purely as a side: in C and C++, the conditional statement is written using if and else, while the conditional expression is written with a ternary operator ? and :. ending a sentence with . is a must. Including a period directly after a syntactic construct about ? and : is .. jarring because it is possible to attempt to read this as :. as an atomic construct in the language. Or even worse, the three-dots pyramid in some mathematical proof notations.

AdieuToLogic 3y ago
> Also, I always find it interesting the ternary operation is constructed in statements/expressions in ? ... : notation but actually has "two" operators there. the ? is the conditional, the : is the binary-choice. It's a language syntax choice which "side" is true or false and it is also true that you can't construct statements in : without a prior ? but .. its hardly a single operator in syntax terms if it has two disjoint components. := is an unambiguous single operation. condition ? x : y is ... not. It's definedly ambiguous! In C++, the lexical construct you describe is an atomic operator[0] and neither an expression nor a statement: The first operand of the conditional operator is evaluated and contextually converted to bool. After both the value evaluation and all side effects of the first operand are completed, if the result was true, the second operand is evaluated. If the result was false, the third operand is evaluated. 0 - https://en.cppreference.com/w/cpp/language/operator_other https://en.cppreference.com/w/cpp/language/operator_other
- ggm 3y ago
  I took my comments about ?...: notation out. Basically, at a syntactic level its tempting to regard ? as "the operator" and : as some other operator but really the ternary operation only exists as some hypothetical function in 3 arguments: ternary(condition, true-path, false-path) which executes either true-path or false-path depending on condition. But in notational terms, how "big" condition and true and false parts are is rather unconstrained, so you wind up with the ? and the : widely separated. They aren't operators in the higher sense: they're the syntax which forms the ternary operation as a whole over the expression and it's condition. Lexing bleeds into syntax and syntax bleeds into semantics. :. is a possible faux-pas in lexing the sentence around the ?...: construct because of :. being unfortunate.

foderking 3y ago

this is actually a good read

d_christiansen 3y ago
Thank you! I hope you enjoy the rest of it.

revskill 3y ago

Is this production ready ? How about performance (comparison with Rust)

siknad 3y ago
Lean is currently moving to the 4th iteration which is the first intended to be a general-purpose programming language. It "is currently being released as milestone releases towards a first stable release". For now the main goal is to port mathlib to the new version, and then they will concentrate on the compiler. So it is not production ready. But that doesn't mean it is not suitable for building any programs now. There is a simple raytracer written in Lean [1]. I have built a chip8 interpreter with it and the only problem was the lack of an ecosystem, meaning I had to build the necessary libraries myself. Now it has a RC GC and boxes everything >= 64 bits (including struct fields and IO/ST results), and as the compiler isn't polished it is probably significantly slower. In the referenced raytracer repo you can find rendering time compared to the C implementation (Lean is 25x slower, but that was a year ago). [1] https://github.com/kmill/lean4-raytracer https://github.com/kmill/lean4-raytracer
reuben364 3y ago
While Lean4 is meant to be much more of a general purpose language than it's predecessor, it is still built with being a proof assistant in mind. That being said it is self hosted and has been in development and use for quite some time, which says something of it's readiness. Tooling around it great (it is installed with a rustup fork called elan). As far as performance, it uses a particular version of ref-counting that allows mutation of unique references based on run-time tracking rather than compile time. If you accidentally keep a reference to an array and modify it, then you end up copying it rather than just mutating it.

theresistor 3y ago

I'm interested to know why I would want to learn Lean if I'm already familiar with Idris.

siknad 3y ago
Big: * tactics (proof scripts are a lot easier than manual proving) * syntax extensibility (Racket-like, supports custom elaboration/delaboration) * mathlib (library of formalized math) * tooling (can't say it's better, I haven't used Idris, but it's at least a lot nicer than Agda's: rustup-like version manager `elan`, own build system `lake`, official vscode extension supporting mini web apps which can interact with the code) Small things I can remember: * do-notation with early return and imperative loops * easier termination proof handling (provide some expression using function arguments with `decreasing_by` and prove it's decreasing with `termination_by` block, which may be automatic even for non-structural recursion because of some built-in tactic)
- dmytrish 3y ago
  Regarding tactics: I started with Coq and I felt for a long time that I had no idea what tactics actually do. Proofs with tactics look nice on the surface, but I really did not like hidden state and hidden actions. Redoing some proofs in Lean by construction of proof terms was eye-opening, it's just functional programming with dependent types! I still think that teaching with tactics first without exposing proof terms is a mistake. I've learned to see the value of tactics later, again thanks to Lean: there are proofs that are more natural in the tactics style. Sometimes a mixed approach is ideal: growing intermediate proof terms from the premises and then wrangling the hypothesis with tactics to meet the lemmas.
d_christiansen 3y ago
Lean occupies a different point in the design space. Its type theory is simpler and more conservative, its metaprogramming system is more reminiscent of Racket's (including hygienic procedural macros), and the focus on supporting professional mathematicians gives a different feel to the community and libraries. I think both are worth knowing, but either is great to learn. I hope the two projects learn more from each other in the future.

calrizien 3y ago

Is there a public compendium of lean proofs? More specifically, has Euclid's Elements been translated into lean?

arlort 3y ago
Is this what you're looking for? https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib
dmytrish 3y ago
There's Mathlib: https://leanprover-community.github.io/mathlib_docs/index.html https://leanprover-community.github.io/mathlib_docs/index.ht... I was stunned when I discovered it, because it does exactly what its name suggests: it's a huge library of math proofs available as a library in Lean.

sullyj3 3y ago

Does lean have an analogue to hoogle?

fogof 3y ago
For searching using search terms for theorems in mathlib, there is the mathlib documentation page (for Lean 3 https://leanprover-community.github.io/mathlib_docs/ https://leanprover-community.github.io/mathlib_docs/ and Lean 4 https://leanprover-community.github.io/mathlib4_docs/ https://leanprover-community.github.io/mathlib4_docs/). To find theorems by type, I find the best way is to use the `library_search` tactic from inside Lean itself.