Learn You an Agda
williamdemeo.github.io
Learn You an Agda
1–10 of 72 posts
Re: Learn You an Agda
#2I really like these "learn you a" books.
I have no reason why but I just like the freaking pictures. It keeps me going. It's like a children book but it also teaches me the subject I like, programming languages.
Re: Learn You an Agda
#3How does Agda compare to the likes of Clojure, Haskell, ML, Scheme etc? What are the best reasons to learn it?
Re: Learn You an Agda
#4Ah 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.
Re: Learn You an Agda
#5How does Agda compare to the likes of Clojure, Haskell, ML, Scheme etc? What are the best reasons to learn it?
The article covers this here http://williamdemeo.github.io/2014/02/27/learn-you-an-agda/#...
Some excerpts:
> Agda is a programming language that uses dependent types ... you can actually include values inside a type. For example, the List type constructor can be parameterized by both the type of its contents and the length of the list in question ... . This allows the compiler to check for you to make sure there are no cases where you attempt to call head on a potentially empty list, for example.
> If I can come up with a function of type Foo -> Bar (and Agda says that it’s type correct) that means that I’ve written not only a program, but also a proof by construction that, assuming some premise Foo, the judgment Bar holds.
> Proofs work in concurrent scenarios. You can’t reliably unit test against race conditions, starvation or deadlock. All of these things can be eliminated via formal methods.
> Thanks to Curry-Howard, Agda can also be used as a proof language, as opposed to a programming language. You can construct a proof not just about your program, but anything you like.
Re: Learn You an Agda
#6I really like these "learn you a" books. I have no reason why but I just like the freaking pictures. It keeps me going. It's like a children book but it also teaches me the subject I like, programming languages.
On top of the pictures, the examples are a lot more fun than foo and bar. Here's (part of) how Learn You a Haskell introduces map:
ghci> map (++ "!") ["BIFF", "BANG", "POW"]
["BIFF!","BANG!","POW!"]Re: Learn You an Agda
#7Ah 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 a…
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:
Re: Learn You an Agda
#8Recently learned this language in a functional programming course. Very cool language. The Curry-Howard Isomorphism proves that programming languages are equivalent to mathematical proofs and you can really feel it here. I could see this language being very useful in math-y applications such as cryptography and verification.
Re: Learn You an Agda
#9Languages that use types for elaborate proofs always seem to me like they only prove the most uninteresting properties of programs, namely the parts that deal with data transformations. Not that data transformations aren't important, but the properties they need to preserve are usually easy to be convinced of without any assistance by the compiler.
At the end of the day, programs are written for their side effects (unless your program is a compiler, which is the classical example of an "interesting", non-trivial data transformation, and possibly the only example). What I'm most interested in is proofs that, say, in a concurrent environment, a function that closes a socket will never be called as long as there are pending tasks to write to the socket. Or, because I write concurrent data structures, I'm interested to prove that a certain function will eventually release all locks it acquires. Are there any such languages?
I've heard of effect systems, but I couldn't find enough information on them. Are effect systems capable of the kind of proofs I'm interested in? Are there practical programming languages with powerful effect systems?
EDIT: Some Googling yielded this: http://lambda-the-ultimate.org/node/4768 tldr: Not yet.
EDIT: At least the lock proof seems to be implemented as one of Java 8's pluggable type systems: http://types.cs.washington.edu/checker-framework/current/che...
It lets you add a type (Java 8's pluggable types are intersection types) to a function called @EnsuresLockHeld(locks...) that proves some locks will be held when a function returns and even @EnsuresLockHeldIf(locks..., result) that proves a function grabs certain locks if its boolean result is equal to the one specified in the type.
Re: Learn You an Agda
#10Ah 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 a…
I'm not sure if they will meet your standards, but Idris and ATS strive to be practical dependently typed languages:
http://www.ats-lang.org/Examples.html http://www.idris-lang.org/