Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Functional Programming in Lean

leanprover.github.io

Post reply on HN
Print view View original

1–10 of 40 posts

Re: Functional Programming in Lean

#2

Post by d_christiansen »

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.

Re: Functional Programming in Lean

#4

Post by mdm12 »

d_christiansen wrote: post #2

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.

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!

Re: Functional Programming in Lean

#5

Post by ykonstant »

d_christiansen wrote: post #2

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.

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.

Re: Functional Programming in Lean

#6

Post by epgui »

mdm12 wrote: post #4
d_christiansen wrote: post #2

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.

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!

Agda and Idris both also position themselves similarly.

Re: Functional Programming in Lean

#7

Post by ggm »

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.

Re: Functional Programming in Lean

#8

Post by [deleted] »

d_christiansen wrote: post #2

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.

[deleted]

Re: Functional Programming in Lean

#9

Post by AdieuToLogic »

ggm wrote: post #7

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…

> 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

Re: Functional Programming in Lean

#10

Post by ggm »

AdieuToLogic wrote: post #9
ggm wrote: post #7

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…

> 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 d…

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.

Post reply on HN