▲ 161 points
back
24 comments
For enlightenment learn Agda. For transcendence, learn Idris ;)
I would like to learn either Idris or Agda for their relationship to mathematics, but I am tempted by Idris also being able to do general programming with its compile targets. How does Agda compare to Idris on this point?
Runtime performance for Agda... well, it leaves a lot to be desired, at least with respect to the MAlonzo compiler. For example, operations on the natural numbers à la Data.Nat get very slow very quickly-- but while the representation used by Data.Bin speeds things up a lot, you just can't do the same Peano-style structural induction on it.
My understanding is that Agda puts much less emphasis on general programming. It's more focused on proving.
>Agda’s logic is constructive, which means it’s impossible to prove the statement that all statements are either true or false, . This proposition is called the law of the excluded middle. This makes it impossible to perform, for example, a general proof by contradiction, or other similar “classical” proofs from mathematics. There is a large philosophical debate among mathematicians (those who follow Hilbert, and those who follow Brouwer) as to which is better
Still, for a subset of statements and properties it is possible to construct a law of excluded middle, but it has to be a constructive proof. The whole idea of Constructive Mathematics is that you have to show a proof for both, the statement and it's negation to hold their respective truth values. The impossibility to proof the first statement, that of all statements the negation is implied, is surely tautologic, assuming it would hold true for most of all statements, just not a class the opening one is part of. This class is an empty element.
I would basically assume this means nonsense statements can be constructed, but they can't be used in constructive proofs. It doesn't imply that there has to be a class of nonsense statements where the opposite still holds value. I'm cautios of the definition for statements like there or in the multiple incarnations of the liars paradox (whats the latin plural). IE. a statement should by definition be provably correct either in positive or negative logic, hi and low to use ee terms, and one should imply the other polarity (edit: just not by using negation, because that's the relation you want to prove, without circular logic). The empty element is like null, but what logic set the true ^ negative or just the true statements have to be defined in I dont know.
Interesting to know that there is a tool for this kinda maths, I was under the impression that the debate tends to inductive methods, but here we have intuitionistic (constructive) logic, I take it.
I'm not sure everything you're talking about, but it's relatively easy to reason about constructive logic by abandoning the idea that your logic is one of "truth and falsehood"—which are, by modern, western intuition mutually exclusive options—but instead one concerning evidence.
One might believe that the Collatz conjecture is true or false, but we certainly lack evidence for either case today. This isn't exactly three value logic, but instead something else. A logic which incorporates the notion of time and communication of proof.
> which incorporates the notion of time and communication of proof.
Certainly constructive logics (typically) incorporate a notion of evidence/proof. But constructive logics don't incorporate notions of time or communication (of proof, or in general).
Yeah, to be clear, those notions aren't internalized... they just bring into clarity the need for those processes to happen in the meta level.
>Still, for a subset of statements and properties it is possible to construct a law of excluded middle, but it has to be a constructive proof. The whole idea of Constructive Mathematics is that you have to show a proof for both, the statement and it's negation to hold their respective truth values. The impossibility to proof the first statement, that of all statements the negation is implied, is surely tautologic, assuming it would hold true for most of all statements, just not a class the opening one is part of. This class is an empty element.
It's actually a lot simpler than that. Proofs in constructive logic have computational content, so the actual counterexample to the Law of the Excluded Middle is the Halting Problem. To state the Law of the Excluded Middle constructively is to say, "I possess a Turing machine which can answer yes-or-no to any given proposition in finite time", which is a trivially false statement (particularly where concerning sufficiently large infinities).
> paradox (whats the latin plural)
I think it's "paradoxa", but I've never seen anyone use that in English. Just go with "paradoxes" :-)
This was one of my first encounters with Agda, and it's a language I've developed something of a soft spot for. I highly recommend playing with it if you have any interest in Haskell or ~undergraduate-level pure mathematics.
I also found the following very useful:
* A Demonstration of Agda (https://www.youtube.com/watch?v=8WFMK0hv8bE)
* Agda Tutorial (http://people.inf.elte.hu/divip/AgdaTutorial/Index.html)
That was the most enjoyable and accessible introduction to Agda that I have ever seen. If you are the creator, please continue the development of the tutorial.
> At the time of writing, it is only really feasible to edit Agda code using Emacs.
Why?
It's really just basic editor support. Agda is quite an interactive programming language, so you need lots of shortcuts, syntax highlighting, autofilling etc in order to get productivity at all (especially since you're constantly moving stuff in and out of a repl)
https://youtu.be/pP7ynVdVY9A?t=13m gives a decent example.
As to why support isn't in other editors, it's probably a combination of: more code to support, no one wants to write it, and the fact that Agda is less amenable to being sped up by efficient usage of editors (as it is a more interactive process with less copy pasting).
I have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has neither. Rather I find these bells and whistles distracting — and prefer giving my complete attention to the task at hand.
I think that writing agda code interactively in Emacs is fine, but it is certainly not the only way to write good agda code. In fact writing without the interactive support encourages better code structure. One is more likely to factor a complicated line into several help terms (using 'where', for example), which makes the code more readable.
Emacs is the only officially supported interactive Agda environment, as other people have noted.
However, I have written a lot of Agda code in other editors (acme and vim). It is certainly feasable to do! In fact I find that it improves my code quality not to use the interactive features. When in interactive mode, I blindly chase the goal trying to get the correct type, and often end up going long detours. When I am on my own I get a better overview of the situation, and can often see the shortest path.
That said, I wish they would continue to support agda interactive mode on the command line, as it is nice to be able to evaluate expressions in context of a hole.
Writing unicode is a breeze with XCompose, in any UTF8-enabled editor. I found a nice XCompose file based on the Plan 9 keyboard file, by Pmarin. It can be downloaded from «Greg 'Groggy' Lehey»'s site:
Writing Agda is a very interactive experience. The only IDE that provides this interactivity at present is Emacs. If you take a look at some Youtube clips of people editing Agda you'll see why you would want an IDE. Not that this can't be done elsewhere, just that it hasn't been done yet.
I think this is (at least part of) why:
"Another thing that sets Agda apart from other languages is its extensive use of unicode to make mathematical constructs more natural."
APL called and is a bit miffed.
They didn't have Unicode back then :-)
Does Agda have any significant proof automation yet compared to say Coq? If not, how practical is it to use?
there is an agda shell for interactice proving in emacs, with some automations.
convenience offered by agda-mode: automatic generation of case analysis, refinement of holes, autocompletion of code based on types to name a few. http://lambda.jstolarek.com/2013/12/idris-first-impressionsi...
don't forget about https://www.fstar-lang.org/
First step: Learn Haskell :D