These are my first impressions of the Agda programming language after researching it in some depth but before writing any actual Agda programs.
If you only want the highlights, just read the Executive Summary. If you also want to see supporting material and notes, continue reading further.
Agda, by virtue of it possessing a dependent type system, makes it a very powerful programming language. Agda is distinguished from its cousins like Coq in that it makes more of an effort at being a programming language as opposed to being merely a proof assistant. Certainly worthy of study for the purpose of learning what a truly powerful type system is capable of expressing.
However Agda I judge to not presently be worthy as a full production-quality programming language, suitable for long term development. My reasons:
Library discoverability is also impaired.
A lack of a forward-compatibility promise from the standard library is not acceptable for long term development.
Other tripping points:
Such API documentation can be used effectively but it is not the format that the larger programming community expects (i.e. styled HTML) and is lacking in aesthetic appeal.
Agda only appears to have integration with the Emacs code editor. In particular there is no obvious integration with any GUI code editors, like Sublime Text. And such editor integration is necessary at minimum for the Unicode-style input that Agda requires.
I expect that many of these shortcomings will be addressed over time.
In the meantime, as I mentioned before, I think Agda is still worthy of investigation for expanding one’s knowledge of what is possible in a powerful type system. In fact, any language where you can do something like write a sorting function that both works and proves itself to be a correct implementation in the same stroke deserves a closer look.1
Official website of Agda is http://wiki.portal.chalmers.se/agda/pmwiki.php:
Uses Unicode operators all over the place. Nice to read. Tricky to type. Even library developers use them.
Agda should not be used on Windows. None of the core release maintainers run Windows.2
Strongly expects that you use Emacs, as Agda provides its own interactive Emacs mode.
Apparently the Agda community is sufficiently small that all libraries (of significance?) can be listed comfortably on the main Agda website at http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries.
Only two libraries under the https://github.com/agda umbrella have been updated within the last year. One of them is the Agda standard library. Not a good sign of activity.
Libraries do not carry external documentation. Instead all documentation is within the source code itself. The expectation is that you will use the Agda emacs mode to jump around between modules and explore to find what you want. Not ideal but serviceable.
Readers of the documentation are assumed to have high mathematical training. I see terms like “communative semiring”, “coinductive”, “lemma”, and “decidable”.
This is an FRP implementation in Agda. I’ll look at it because I’ve been working in FRP systems recently (i.e. Elm). And because I’d like to see how well libraries are packaged by the Agda community.
“Beh” is short for “behavior” and is equivalent to an Elm Signal.
I note that there is no API documentation whatsoever for the module. You have to browse through the examples in the source tree manually. This suggests that either Agda has no doc generator tool (likely!) or this library author simply didn’t bother to generate docs for the public to read.
Virtually no comments.
Not going to look at this closely due to the lack of activity.
Agda is used in quite a number of academic papers. Certainly more papers than actual libraries, so far as I can tell. There’s a whole list of papers that use Agda.
Describes an FRP system that is slightly more powerful than that of Yampa. It defines a type system around FRP that guarantees that FRP programs written within the type system will necessarily continue to make progress (i.e. not deadlock). (It is possible for an FRP system to deadlock if its signal graph get reconfigured into certain kinds of loops.) It also eliminates the distinction between continuous and discrete signals, reducing one class of errors. Furthermore it allows programs to include feedback loops and uninitialised signals in an FRP program, whilst guaranteeing evaluation progress at the type level.
Hard to find books on Agda. I get nothing.
However I do see some books on Coq, which Agda is inspired by. Let’s not get distracted by those at the moment.
Appears to be the original paper that introduced the Agda programming language. Or at the very least a fairly complete description of the language along with tutorial-style content.
“domain-specific embedded type systems”
Aims to describe at a high-level how dependently typed languages work at the level of theory, without going into too many details. Uses Agda as a concrete language to work with.
I first recognized that you could write this kind of provably correct sorting function when I read these slides at swan.ac.uk. You end up having a sorting function with a signature like
sort : (inList : List a) -> (outList : List a, IsSorted outList, EqElements inList outList).
IsSorted outList type represents proofs that
outList is sorted. Thus the existence of a member of the
IsSorted outList type proves that
outList is sorted. Similarly the
EqElements inList outList is a proof type where
outList are proven to have equal elements.
See also the dedicated article at mazzo.li↩