From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Amin Bandali Newsgroups: gmane.emacs.help Subject: Re: [OFFTOPIC] Re: Invoking a function from a list of functions Date: Tue, 11 Dec 2018 13:48:42 -0500 Message-ID: <87d0q73nn9.fsf@aminb.org> References: <67c4a534-d41c-4736-8839-c2dbbdf7f9c2@googlegroups.com> <2da7504a-8bbf-41b9-993e-a7bacd6c97b2@googlegroups.com> <20181116114002.3ba6bcc8dc1e699ba58e08b8@speakeasy.net> <20181119172358.802ce30c54f2fd20f8c300c4@speakeasy.net> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1544554050 2884 195.159.176.226 (11 Dec 2018 18:47:30 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 11 Dec 2018 18:47:30 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) Cc: help-gnu-emacs@gnu.org To: Rusi Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Tue Dec 11 19:47:26 2018 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gWn42-0000fI-A3 for geh-help-gnu-emacs@m.gmane.org; Tue, 11 Dec 2018 19:47:26 +0100 Original-Received: from localhost ([::1]:40853 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gWn68-0003Wn-R5 for geh-help-gnu-emacs@m.gmane.org; Tue, 11 Dec 2018 13:49:36 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:58916) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gWn5Q-0003Tq-Nv for help-gnu-emacs@gnu.org; Tue, 11 Dec 2018 13:48:53 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gWn5P-0001LL-QA for help-gnu-emacs@gnu.org; Tue, 11 Dec 2018 13:48:52 -0500 Original-Received: from fencepost.gnu.org ([2001:4830:134:3::e]:42805) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gWn5H-00015J-9c; Tue, 11 Dec 2018 13:48:45 -0500 Original-Received: from wn-res-nat-129-97-125-0.dynamic.uwaterloo.ca ([129.97.125.0]:47336 helo=localhost) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gWn5G-0006qD-TG; Tue, 11 Dec 2018 13:48:43 -0500 In-Reply-To: (Rusi's message of "Wed, 28 Nov 2018 06:14:38 -0800 (PST)") X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.org gmane.emacs.help:118970 Archived-At: On 2018-11-28 6:14 AM, Rusi wrote: > Thanks for pointing out lean to me > [And not just because its spelt L=E2=88=83=E2=88=80N !] :) No worries! > Do you have a good comparison of the contenders lean, agda, idris isabell= e(?) etc? I haven=E2=80=99t personally used all of them, so I can=E2=80=99t 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=E2=80=99s 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=E2=80=99d found Agda a bit hard to use because of i= ts limited proof language. Though, he=E2=80=99d found pattern matching in Agd= a 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 =E2=80=98general purpose=E2=80=99 env= ironments not geared towards only one of programming or theorem proving, but both. Further, Lean borrows many niceties of the others, including Agda=E2=80=99s pattern matching, Haskell=E2=80=99s type classes like Applicative Functors = and Monads and convenient syntactic sugar like the do notation, Coq=E2=80=99s C= IC, 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=E2=80=99s 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.