Ah yes, dependent types. They tried to teach this at my university because some researchers there were working on it. Too bad they didn't bother to teach something more useful, like what malloc and free do.
But let's see. Perhaps the field has become less wonkish and more relevant to real programmers in the last ten years.
Most language tutorials start with the typical “Hello, World” example, but this is not really appropriate for a first example in Agda. Unlike other languages, which rely on a whole lot of primitive operations and special cases for basic constructs, Agda is very minimal - most of the “language constructs” are actually defined in libraries.
That sounds reasonable ...
Agda doesn’t even have numbers built in, so the first thing we’re going to do is define them
That's much less reasonable ...
This is a very elegant way to define infinitely large sets. This way of defining natural numbers was developed by a mathematician named Giuseppe Peano, and so they’re called the Peano numbers .... Now we can express the number one as suc zero, and the number two as suc (suc zero), and the number three as suc (suc (suc zero)), and so on.
Oh dear. This is a new use of the word elegant I have not encountered before.
I was expecting the next stage of the tutorial to describe how to make numbers in Agda resemble number systems actually used by humans, or even machines, but no such luck. They stick with a Lisp-style Peano representation throughout the entire thing. Having defined an entirely unworkable method of representing integers because their standard library apparently doesn't do so (?!) they then go on to prove things like 1 + 1 == 2.
Yeah, I think I'll skip. Perhaps in another few decades someone will have bothered to make a dependently typed language that doesn't use untypeable characters as part of its syntax, and has an integer type built in, and we'll all get awesome statically checkable code for free. Until then I'm gonna stick with FindBugs.
Wow, you are just radiating ignorance; I don't even know why I'm wasting my breath. Nonetheless,
> Oh dear. This is a new use of the word elegant I have not encountered before.
The Peano numbers are elegant because they correspond directly with induction. Agda is first and foremost a proof assistant, so it's natural that we lean towards things that help as write our proofs. This is not "Lisp-style" at all, it's a mathematically consistent way of defining natural numbers. The idea extends further with ornamentation to model lists and other data structures.
> Having defined an entirely unworkable method of representing integers because their standard library apparently doesn't do so (?!) they then go on to prove things like 1 + 1 == 2.
I don't know what's "unworkable" about Paeno arithmetic. Yes, it's not the most efficient representation, but you're working in a proof engine, so that is secondary to our concerns. Furthermore, Agda has {-# BUILTIN #-} pragmas that let us switch out this data type with something that is more optimal. We don't use "the number system actually used by humans" (whatever that is) or machines, at least traditionally, because they just make the proofs harder.
> Perhaps in another few decades someone will have bothered to make a dependently typed language that doesn't use untypeable characters as part of its syntax, and has an integer type built in
Yea, some of us did "bother" - you're looking for Idris. But I'd really rather you didn't join us.
I know Agda isn't really a programming language, but then why is this book trying to claim it is? It says at the start:
_Agda is a programming language_
That's the standard it sets right from the first chapter. It then goes on to say that this programming language doesn't have numbers.
If the book had said, "Agda is a proof assistant for CS and mathematics researchers to research inductive logic" then I'd have been much less harsh on it, but whilst this book is claiming it's a tool for programmers I will judge it by that standard. And by that standard representing numbers and even forcing you to type them in as (suc (suc (suc (zero))) is not elegant.
As I see it, this is not so much a book at this stage as an introductory tutorial written by someone as they were learning Agda (about four years ago I think), as a contribution to the community to help other beginners. As such, one of the (unstated) assumptions is that the reader is already motivated to learn about programming with dependent types.
The early examples you see with inductive structures such as Nat are about learning the foundations, and you can't go on to do anything especially interesting without a solid understanding of the foundations. Its structure often also turns out to have a convenient correspondence with more realistic data structures, such as lists (their length) and trees (their depth).
I do sometimes wonder if we should start using something more obviously useful as an introductory example though. There's plenty of possibilities, and programmers aren't generally going to be using Nats in practice (I rarely do).
I don't use Agda myself (I use Idris, which is similar but is more directly aimed at general purpose programming) but I do know that it has primitive types...
Anyway, there's all kinds of interesting work going on at the minute which goes way beyond these introductory examples. For example, we're working on a way of specifying and verifying implementations of communication protocols (https://github.com/edwinb/Protocols), which we'd like to apply to cryptographic protocols when we've made some more progress. You can hear me waffling on about that, as well as about how we deal with stateful systems in general, here: https://www.youtube.com/watch?v=rXXn4UunOkE&feature=youtu.be
I post this mainly because I suspect I'm one of the wonks who was researching dependently typed programming at your university ten years ago. At the time, there was lots of foundational work to do, and there is still lots to do before it's industrial strength, but we've made a lot of progress, and I think the goal is worth striving for.
Agda is well-suited to computing with values that carry around various formally-checked properties. That's useful to some people for some tasks. If it's not suited to whatever you're doing, then don't use it; I presume your projects don't all use Java, Bash, Prolog, Python, COBOL, Pure, Unlambda and MATLAB at the same time; well, just add Agda to that list.
Agda and most other dependently-typed languages (e.g. Coq) weren't really designed for "real programmers": they're research-oriented systems for real computer scientists to explore cutting edge ideas in logic and PLT.
If you're interested in a "practical" dependently-typed language, check out Idris:
But let's see. Perhaps the field has become less wonkish and more relevant to real programmers in the last ten years.
Most language tutorials start with the typical “Hello, World” example, but this is not really appropriate for a first example in Agda. Unlike other languages, which rely on a whole lot of primitive operations and special cases for basic constructs, Agda is very minimal - most of the “language constructs” are actually defined in libraries.
That sounds reasonable ...
Agda doesn’t even have numbers built in, so the first thing we’re going to do is define them
That's much less reasonable ...
This is a very elegant way to define infinitely large sets. This way of defining natural numbers was developed by a mathematician named Giuseppe Peano, and so they’re called the Peano numbers .... Now we can express the number one as suc zero, and the number two as suc (suc zero), and the number three as suc (suc (suc zero)), and so on.
Oh dear. This is a new use of the word elegant I have not encountered before.
I was expecting the next stage of the tutorial to describe how to make numbers in Agda resemble number systems actually used by humans, or even machines, but no such luck. They stick with a Lisp-style Peano representation throughout the entire thing. Having defined an entirely unworkable method of representing integers because their standard library apparently doesn't do so (?!) they then go on to prove things like 1 + 1 == 2.
Yeah, I think I'll skip. Perhaps in another few decades someone will have bothered to make a dependently typed language that doesn't use untypeable characters as part of its syntax, and has an integer type built in, and we'll all get awesome statically checkable code for free. Until then I'm gonna stick with FindBugs.