Re: [OFFTOPIC] Re: Invoking a function from a list of functions

[Amin Bandali]

On 2018-11-28  6:14 AM, Rusi wrote:
> Thanks for pointing out lean to me
> [And not just because its spelt L∃∀N !]

:) No worries!

> Do you have a good comparison of the contenders lean, agda, idris isabelle(?) 
> etc?

I haven’t personally used all of them, so I can’t talk with certainty;
so please take this with a grain of salt.  Also, I think each of these
languages are great tools in their own light.

That said, the first three you mentioned (Lean, Agda, and Idris) are
based on dependent type theory, whereas Isabelle is based on simple type
theory.  I think that’s a fairly distinguishable difference.

Of the ones based on dependent type theory, Agda and Idris give me the
impression of being more closer to a programming language with dependent
types than a theorem prover.  A friend of mine that does a lot theorem
proving once told me he’d found Agda a bit hard to use because of its
limited proof language.  Though, he’d found pattern matching in Agda to
be really good and more convenient than Coq.  Lean and Coq, both being
based on the Calculus of Inductive Constructions flavour of dependent
type theory, seem to come off as more ‘general purpose’ environments not
geared towards only one of programming or theorem proving, but both.

Further, Lean borrows many niceties of the others, including Agda’s
pattern matching, Haskell’s type classes like Applicative Functors and
Monads and convenient syntactic sugar like the do notation, Coq’s CIC,
etc.  Another characteristic that makes Lean very exciting is its
meta-programming facilities and the ability to write tactics and extend
the language in Lean itself, e.g. unlike Haskell’s Template Haskell.
Further, two of the Lean core developers are working on rewriting more
pieces of currently-writtten-in-C++ of Lean in Lean for the upcoming
Lean 4, exposing more of the parser and internals for use by external
tools like text editors (including our favourite GNU Emacs :-)) and
embedding of arbitrary domain-specific languages in Lean.


Here are some links with vastly more information than my rant above :)

https://leanprover.github.io/papers/system.pdf
https://leanprover.github.io/talks/stanford2017.pdf
https://leanprover.github.io/presentations/20181012_MSR/
https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/
https://www.reddit.com/r/Idris/comments/6qv5c6/comparison_between_idris_and_agda/
https://www.functionalgeekery.com/episode-62-lars-hupel/

HTH.