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

31–40 of 40 posts

Re: Functional Programming in Lean

#31

Post by siknad »

epgui wrote: post #6
mdm12 wrote: post #4

Earlier quoted context omitted.

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.

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.

Re: Functional Programming in Lean

#33

Post by dmytrish »

calrizien wrote: post #28

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

There's Mathlib: 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.

Re: Functional Programming in Lean

#34

Post by dmytrish »

siknad wrote: post #19
theresistor wrote: post #17

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

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…

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.

Re: Functional Programming in Lean

#36

Post by fogof »

sullyj3 wrote: post #35

Does lean have an analogue to hoogle?

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/ and Lean 4 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.

Re: Functional Programming in Lean

#37

Post by epgui »

siknad wrote: post #31
epgui wrote: post #6

Earlier quoted context omitted.

Agda and Idris both also position themselves similarly.

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.

You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).

Re: Functional Programming in Lean

#38

Post by AdieuToLogic »

saghm wrote: post #12
AdieuToLogic wrote: post #9

Earlier quoted context omitted.

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

> its hardly a single operator in syntax terms if it has two disjoint components I don't think "operator in syntax terms" is nearly as well-defined as OP thinks. Why couldn't `?` be parsed as half an operator and `:` as the other half? There's no rule that says a parser has to call each distinct symbol token its own "operator". In fact, I'd argue that the only reason this might seem seem like a rule is that almost al…

> Why couldn't `?` be parsed as half an operator and `:` as the other half?

Because the language defines it to be an atomic operator named "conditional operator." As to the implications of that definition, please read the referenced link[0].

> In fact, I'd argue that the only reason this might seem seem like a rule is that almost all of the other operators in common use are either unary or binary, making it easy to use a single token for the operator itself.

It is "a rule" because that is how the language is defined. If you'd like to argue otherwise, please feel free to do so with the C++ standards committee.

0 - https://en.cppreference.com/w/cpp/language/operator_other

Re: Functional Programming in Lean

#39

Post by AdieuToLogic »

ggm wrote: post #10
AdieuToLogic wrote: post #9

Earlier quoted context omitted.

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

> I took my comments about ?...: notation out.

I see that now. When I was composing my comment, they were there which is why they were quoted.

My apologies for how the response timing transpired.

Re: Functional Programming in Lean

#40

Post by saghm »

AdieuToLogic wrote: post #38
saghm wrote: post #12

Earlier quoted context omitted.

> its hardly a single operator in syntax terms if it has two disjoint components I don't think "operator in syntax terms" is nearly as well-defined as OP thinks. Why couldn't `?` be parsed as half an operator and `:` as the other half? There's no rule that says a parser has to call each distinct symbol token its own "operator". In fact, I'd argue that the only reason this might seem seem like a rule is that almost al…

> Why couldn't `?` be parsed as half an operator and `:` as the other half? Because the language defines it to be an atomic operator named "conditional operator." As to the implications of that definition, please read the referenced link[0]. > In fact, I'd argue that the only reason this might seem seem like a rule is that almost all of the other operators in common use are either unary or binary, making it easy to u…

From what I can tell, the link doesn't seem to disagree with me? The quote I was responding two characterized `?` and `:` as separate operators, and I argued that they were in fact one operator with two separate syntax tokens. The link you provided describes `?` and `:` as a single operator, which is consistent with what I said. I suspect that the C++ standard doesn't disagree with me that half of two is one, which would mean that `?` is half of the operator, and `:` is the other half.
Post reply on HN