10 ms·

Learn You an Agda

127 points by bkirwi 12y ago

kxyvr 12y ago
Is there any reason to use Agda over Coq or vice versa?
- cies 12y ago
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVs... You might also want to compare to Idris (and maybe Epigram, but its no longer in development). http://www.quora.com/How-does-Idris-compare-to-other-dependently-typed-programming-languages http://www.quora.com/How-does-Idris-compare-to-other-depende... http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram_or_idris_which_one_to_learn/ http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram... http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/ http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_... http://stackoverflow.com/questions/9472488/differences-between-agda-and-idris http://stackoverflow.com/questions/9472488/differences-betwe... All have pros and cons; i like that Idris can compile to JS (https://raichoo.github.io/posts/2014-01-28-improved.html https://raichoo.github.io/posts/2014-01-28-improved.html)
digitalzombie 12y ago
I 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.
- wlesieutre 12y ago
  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!"]
  - Dewie 12y ago
    I hate foo/bar for some reason. I think it's because it is supposed to be "this is just whatever", and yet they force me to think about Kung Fu, the Foo Fighters and crowbars.
    - Gigablah 12y ago
      I just think of a certain audio player...
    - carapace 12y ago
      You know it's an old military acronym, right? F.U.B.A.R. stands for eFfed Up Beyond All Recognition. (And SNAFU is Situation Normal: All eFfed Up.) ;-)
  - ufo 12y ago
    The official Python tutorial is also a good example of this. Is all Monthy Python references.
Energy1 12y ago
How does Agda compare to the likes of Clojure, Haskell, ML, Scheme etc? What are the best reasons to learn it?
- pmahoney 12y ago
  The article covers this here http://williamdemeo.github.io/2014/02/27/learn-you-an-agda/#what-is-agda-anyway 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.
  - lmm 12y ago
    Is there a comparison to Idris? It sounds like they're very similar, and more of the people I've followed seem to be interested in Idris than Agda.
mike_hearn 12y ago
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.
- wk_end 12y ago
  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: http://www.idris-lang.org/ http://www.idris-lang.org/
- pseudonom- 12y ago
  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.ats-lang.org/Examples.html http://www.idris-lang.org/ http://www.idris-lang.org/
mjfl 12y ago
Recently 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.
pron 12y ago
Languages 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 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/checker-framework-manual.html#lock-checker 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.
- michaelsbradley 12y ago
  Sounds like you are interested in applications of temporal logic for formal verification in software development, which is an area of active research. Prof. David Harel works in that field: http://www.wisdom.weizmann.ac.il/~harel/papers.html http://www.wisdom.weizmann.ac.il/~harel/papers.html Do an in-page search for terms like temporal, behavioral, scenario, LSC, live sequence. By the way, I'm no expert but am interested in similar applications.
  - pron 12y ago
lelf 12y ago
I like to show you the immense beauty of the Agda standard library: http://agda.github.io/agda-stdlib/html/README.html http://agda.github.io/agda-stdlib/html/README.html (all clickable and…you'd better have proper unicode fonts).
- mcbuilder 12y ago
  Even something as mundane as Data.Bool is beautiful, defining False in terms of bottom. I love to look at unicode, but is it a pain to type it in practice, even given emacs?
  - evincarofautumn 12y ago
    I don’t use Agda, but for most mathy Unicode input, I use C-\ (toggle-input-method) and choose TeX mode. Then you can type “\forall\alpha. \alpha \to \alpha” and get back “∀α. α → α”, which is pretty good. There is also C-x 8 RET if you want to type a particular Unicode character by name or code point number.
  - chas 12y ago
    Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0] [0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...
  - tel 12y ago
    Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are. What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like theorem1 : T (1 - 1 == 0) which is somewhat interestingly different from theorem2 : 1 - 1 = 0 in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).
gosub 12y ago
If we can construct a value of a certain type, we have simultaneously constructed a proof that the theorem encoded by that type holds. data _even : ℕ → Set where I do not understand how to interpret this passage. _ even, given a number, returns a type? in this case, zero even is a type, but we have not created any value with that type. What am I missing?
- tmvphil 12y ago
  In his example, `ZERO` is a value of type `zero even`. `ZERO` is the "proof" that zero is even. Of course its not much of a proof, rather its true by definition. Similarly `STEP ZERO` is of type `suc(suc(zero)) even` and thus a "proof" that two is even.
- tel 12y ago
  That's exactly correct. In a Dependently Typed (DT) language like Agda the language of values and the language of types are one and the same. Thus, a function from types to types is exactly the same sort of thing as a function from values to values. In this case we have a third sort of totally-natural-day-old-kind-of-thing: a function from values of ℕ to types (in Set). It's "just" a function from values to types. Now, we annotate values with their types. Thus we might have a new top-level definition something : zero even something = _ where we've used our postfix `even` function to construct a type from the value `zero`. Is this type inhabited? That's a question of proof and programming. Regardless of its inhabitation, though, we can clearly see that the notion of `zero even` simply being a type is sound---that's the nature of function application when the target domain is that of Set!
- shadytrees 12y ago
  An Agda program isn't like a C program; a C program is just a bunch of strings that tells the processor where to go and what to do. An Agda program is, instead, a bunch of strings that one-by-one teaches the typechecker what is true about the world. In the beginning, there was Set, which is the set of all valid types. It's empty (more or less). Then comes along data ℕ : Set This says that the type ℕ, which will be our natural numbers, belongs in Set. Now Set has one valid type, which is ℕ. But ℕ, which is also a type, is empty. And if there's one thing we know about natural numbers, is that there's lots of them. So we must tell it what its members are. We COULD do it like this: zero : ℕ one : ℕ two : ℕ three : ℕ But how tedious would that be? Instead, we use induction: data ℕ : Set where zero : ℕ succ : ℕ → ℕ So zero is a member of ℕ, like before. But the successor of any member in ℕ is also in ℕ. So succ zero, and succ succ zero, and succ succ succ zero. People see the arrow and they think functions. That's not how I think about it. Functions are great, but when I hear function I think C functions, which are tiny little instructions for tiny little machines and don't make any sense in a dependently-typed world. So instead, when I see the arrow, I think of it as a way of telling the type checker this fact: wherever you see the string "succ n", assign it the type ℕ but ONLY IF "n" is also of type ℕ. Think of the arrow as the lambda abstractor, and the space as the lambda applicator. Maybe that helps a little; maybe it hurts a lot. We plunge forward! _+_ : ℕ → ℕ → ℕ zero + n = n (succ n) + m = succ (n + m) More substitution rules. Whenever you see zero + n, the typechecker is allowed to replace it with n. Whenever you see (succ n) + m, it's allowed to replace it with succ (n + m). Allowed, but not required: the typechecker should only use these rules if it needs help typechecking a string it doesn't recognize. We would now like describe even numbers in Agda. Could we just define data even : Set? And thus give Set its second element? No! Because evenness is a proposition! It _depends_ on our other type ℕ, which is where we get our fancy dependently-typed programming from. We really want to say this: data even 0 : Set data even 2 : Set data even 4 : Set But that would be tedious. So instead we say data even : ℕ → Set If the arrow means substitution, like before, we can think about it like this: wherever we see the string "even n", assign it the type Set (a.k.a. let it be a valid type) but ONLY IF "n" has type ℕ. Is that true for any n? Nope. If it were, we would write data even : ℕ → Set where even_everything_is_goddamn_even : (n : ℕ) → even n Instead, we first assume that "even n" is true for no n at all. That's right: a function with an empty domain. We fill in the domain gradually. data even : ℕ → Set where even_zero : even zero even_succ : (n : ℕ) → even n → even (succ (succ n)) First, even zero means that "even zero" is a member of Set. zero is a natural number, so this typechecks. Second, suppose you have n : ℕ. And suppose even n typechecks. Then even (succ (succ n)) also typechecks. It's simply another form of induction, although slightly trickier because we're trying to fill out a proposition. Anyway. Hope that helps more than it confuses. I think Learn You An Agda makes it more confusing that it really is by not explaining Set and by using that weird postfix notation. Set is just Haskell's asterisk kind "*" if you know Haskell; otherwise it's pretty hard to grok for a while. You should also check out Benjamin Pierce's textbook on Coq programming, which expands on a lot of these details. (Coq and Agda and Idris are all pretty much are built on the same ideas.) http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
tomwilde 12y ago
If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them? In case the compiler can do that conversion: is it is programmed to do that for some subset of numeric types or can it infer an optimal binary representation of a value somehow? On the other hand, if they really were represented as lists then I presume this language is intended as purely academic work and has no application in a production environment. Am I wrong?
- Dewie 12y ago
  It's a proof assistant. Not really something you use for number crunching, industry or not.
  - eli_gottlieb 12y ago
    But a proof assistant for numerical programming would be extremely useful.
- chriswarbo 12y ago
  > If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them? I don't think so, but Natural numbers can't be represented as two's-complement "integers"; neither can Integers. There are many ways to encode such numbers if you really want; the easiest are probably "Fin (2^32)" for a type with 2^32 members (easy to convert to/from unary Naturals), or "Vect 32 Bool" for a list of 32 Booleans (easy to do bitwise stuff). You'd need to decide how to truncate the Naturals though; do you take min(x, 2^32 - 1)? Do you take x % 2 ^ 32? Also, note that "S (S (S (S Z)))" isn't really a list; to turn it into a list we'd have to associate some trivial data with each constructor, eg. [NULL, NULL, NULL, NULL].
- hesselink 12y ago
  I always thought the statement {-# BUILTIN NATURAL ℕ #-} binds the inductive definition of ℕ to an efficient implementation. However, googling now I can find no confirmation of this. Does anyone know more?
alphonse23 12y ago
I posted this on lobste.rs and somebody stole my link.... Hackernews always gets so much more comments.
- bkirwi 12y ago
  Not guilty! I picked this one up on Twitter this afternoon, but it's possible the lineage traces back to your lobste.rs post. (I have no lobste.rs account, though not for lack of interest -- while sparse, the comments there seem to be of very high quality.)
- d2xdy2 12y ago
  When are they going to open registration back up on there?
agumonkey 12y ago
First time I read about 'mixfix' operators, one less thing I'll have to invent I guess. https://www.google.fr/search?q=mixfix+notation https://www.google.fr/search?q=mixfix+notation
olderwannalear 12y ago
My thanks OVERFLOWS. For those who are 'older but not quite Learn U Agda vs 'wiser strategies' HELPFUL. Think eric raymond and too bad that perl is just another dead language -- your wisdom though as recompense. When you are older, it becomes EASIER for crunchfit and yes, it sometimes becomes harder to exercise to point of vomit - "ad nauseum' in Latin, but the pain is much easier. Don't you do three hundred (300) pushups a day? So, the routine is simple. Get stuck running Haskell (another bump on the road to the true language of Coq) - go ahead and flame - do the pushups. Then laugh cause it releaxes and then refrshed back to AGDA. PS. Engineering school was arduous and graduate school. The personal private books/research were just hobbies and no I will not mention my name. Even the so-called Yourdon 'death marches' are just a bump on the road. It's worse than some females - over the period of a 'big city man.' - go ahead flame - Just take code from arxiv, run it in Haskell and Agda and there are only three explanations 1.)the programmer is stupdi - yup that's me 2.)scientific fraud - always possible 3.)the 'compiler' or the strange AMD CPU is fickle in a feminine way? 4.)the language paradigm is 'slightly broken.' 5.) all of the above Fair Warning and Serpents be Here. Haskell, Agda and even Coq are DEFINED as EXPERIMENTAL RESEARCH Languages. Of course, you can always go Python (which version?) and Javascript, which is the bubble gum and string that holds together the Internet.. along with BAsh shellshock. It this why they call it a bit of 'hacking'? PPS. learn to ride bicycle in big city and survived with most of my fingers intact.
eli_gottlieb 12y ago
Ok, that's neat. Is there a proof checker and an editor/IDE other than Emacs' Agda mode? Because I'm probably going to stick with Coq for its tooling.
frontsideair 12y ago
I always wondered about dependent types. Even though it was a little bit too technical for me, at least I have some idea about what it really is. By the way, Z notation rocks.
akkartik 12y ago
It lost me at this point: Type the following into an emacs buffer, and then type C-c C-l (use \_1 to type the subscript symbol ₁): proof₁ : suc (suc (suc (suc zero))) even proof₁ = ? On my newly created emacs setup from the earlier instructions, it's not clear what "type into an emacs buffer" means. Do I create a new file with C-x C-f? Create a new buffer with C-x b? I tried both, and promptly lost agda-mode. I then tried restarting emacs and opening a new .agda file so I get agda mode. Loaded the earlier module and then tried loading this, and it didn't seem to know about suc in the context of this buffer/file. So now I'm lost.
- sjolsen 12y ago
  That should read, "Type the following into the Emacs buffer." You should have something like: module LearnYouAn where data ℕ : Set where zero : ℕ succ : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + m = m (succ n) + m = succ (n + m) data _even : ℕ → Set where ZERO : zero even STEP : ∀ n → n even → succ (succ n) even proof₁ : succ (succ (succ (succ (zero)))) even proof₁ = ?
  - akkartik 12y ago
    Thanks! Can't believe I didn't think of that :/ What's the distinction between C-c C-space and C-c C-r? It looks like the former computes proof obligations for ?s, but what does the latter do? And why couldn't we use the latter in the first instance, to deduce the outermost STEP ? ? Edit: never mind, that did work.
    - sjolsen 12y ago
      > What's the distinction between C-c C-space and C-c C-r? Beats the hell out of me. Here's the docstring for agda2-give (bound to C-c C-SPC): Give to the goal at point the expression in it Here's the one for agda2-refine (C-c C-r): Refine the goal at point. If the goal contains an expression e, and some "suffix" of the type of e unifies with the goal type, then the goal is replaced by e applied to a suitable number of new goals. If the goal is empty, the goal type is a data type, and there is exactly one constructor which unifies with this type, then the goal is replaced by the constructor applied to a suitable number of new goals.

Learn You an Agda

127 points by bkirwi 12y ago

kxyvr 12y ago

Is there any reason to use Agda over Coq or vice versa?

cies 12y ago
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVs... You might also want to compare to Idris (and maybe Epigram, but its no longer in development). http://www.quora.com/How-does-Idris-compare-to-other-dependently-typed-programming-languages http://www.quora.com/How-does-Idris-compare-to-other-depende... http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram_or_idris_which_one_to_learn/ http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram... http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/ http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_... http://stackoverflow.com/questions/9472488/differences-between-agda-and-idris http://stackoverflow.com/questions/9472488/differences-betwe... All have pros and cons; i like that Idris can compile to JS (https://raichoo.github.io/posts/2014-01-28-improved.html https://raichoo.github.io/posts/2014-01-28-improved.html)

digitalzombie 12y ago

I 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.

wlesieutre 12y ago
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!"]
- Dewie 12y ago
  I hate foo/bar for some reason. I think it's because it is supposed to be "this is just whatever", and yet they force me to think about Kung Fu, the Foo Fighters and crowbars.
  - Gigablah 12y ago
    I just think of a certain audio player...
  - carapace 12y ago
    You know it's an old military acronym, right? F.U.B.A.R. stands for eFfed Up Beyond All Recognition. (And SNAFU is Situation Normal: All eFfed Up.) ;-)
- ufo 12y ago
  The official Python tutorial is also a good example of this. Is all Monthy Python references.

Energy1 12y ago

How does Agda compare to the likes of Clojure, Haskell, ML, Scheme etc? What are the best reasons to learn it?

pmahoney 12y ago
The article covers this here http://williamdemeo.github.io/2014/02/27/learn-you-an-agda/#what-is-agda-anyway 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.
- lmm 12y ago
  Is there a comparison to Idris? It sounds like they're very similar, and more of the people I've followed seem to be interested in Idris than Agda.

mike_hearn 12y ago

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.

wk_end 12y ago
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: http://www.idris-lang.org/ http://www.idris-lang.org/
pseudonom- 12y ago
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.ats-lang.org/Examples.html http://www.idris-lang.org/ http://www.idris-lang.org/

mjfl 12y ago

Recently 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.

pron 12y ago

Languages 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 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/checker-framework-manual.html#lock-checker 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.

michaelsbradley 12y ago
Sounds like you are interested in applications of temporal logic for formal verification in software development, which is an area of active research. Prof. David Harel works in that field: http://www.wisdom.weizmann.ac.il/~harel/papers.html http://www.wisdom.weizmann.ac.il/~harel/papers.html Do an in-page search for terms like temporal, behavioral, scenario, LSC, live sequence. By the way, I'm no expert but am interested in similar applications.
- pron 12y ago

lelf 12y ago

I like to show you the immense beauty of the Agda standard library: http://agda.github.io/agda-stdlib/html/README.html http://agda.github.io/agda-stdlib/html/README.html (all clickable and…you'd better have proper unicode fonts).

mcbuilder 12y ago
Even something as mundane as Data.Bool is beautiful, defining False in terms of bottom. I love to look at unicode, but is it a pain to type it in practice, even given emacs?
- evincarofautumn 12y ago
  I don’t use Agda, but for most mathy Unicode input, I use C-\ (toggle-input-method) and choose TeX mode. Then you can type “\forall\alpha. \alpha \to \alpha” and get back “∀α. α → α”, which is pretty good. There is also C-x 8 RET if you want to type a particular Unicode character by name or code point number.
- chas 12y ago
  Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0] [0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...
- tel 12y ago
  Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are. What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like theorem1 : T (1 - 1 == 0) which is somewhat interestingly different from theorem2 : 1 - 1 = 0 in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).

gosub 12y ago

If we can construct a value of a certain type, we have simultaneously constructed a proof that the theorem encoded by that type holds. data _even : ℕ → Set where I do not understand how to interpret this passage. _ even, given a number, returns a type? in this case, zero even is a type, but we have not created any value with that type. What am I missing?

tmvphil 12y ago
In his example, `ZERO` is a value of type `zero even`. `ZERO` is the "proof" that zero is even. Of course its not much of a proof, rather its true by definition. Similarly `STEP ZERO` is of type `suc(suc(zero)) even` and thus a "proof" that two is even.
tel 12y ago
That's exactly correct. In a Dependently Typed (DT) language like Agda the language of values and the language of types are one and the same. Thus, a function from types to types is exactly the same sort of thing as a function from values to values. In this case we have a third sort of totally-natural-day-old-kind-of-thing: a function from values of ℕ to types (in Set). It's "just" a function from values to types. Now, we annotate values with their types. Thus we might have a new top-level definition something : zero even something = _ where we've used our postfix `even` function to construct a type from the value `zero`. Is this type inhabited? That's a question of proof and programming. Regardless of its inhabitation, though, we can clearly see that the notion of `zero even` simply being a type is sound---that's the nature of function application when the target domain is that of Set!
shadytrees 12y ago
An Agda program isn't like a C program; a C program is just a bunch of strings that tells the processor where to go and what to do. An Agda program is, instead, a bunch of strings that one-by-one teaches the typechecker what is true about the world. In the beginning, there was Set, which is the set of all valid types. It's empty (more or less). Then comes along data ℕ : Set This says that the type ℕ, which will be our natural numbers, belongs in Set. Now Set has one valid type, which is ℕ. But ℕ, which is also a type, is empty. And if there's one thing we know about natural numbers, is that there's lots of them. So we must tell it what its members are. We COULD do it like this: zero : ℕ one : ℕ two : ℕ three : ℕ But how tedious would that be? Instead, we use induction: data ℕ : Set where zero : ℕ succ : ℕ → ℕ So zero is a member of ℕ, like before. But the successor of any member in ℕ is also in ℕ. So succ zero, and succ succ zero, and succ succ succ zero. People see the arrow and they think functions. That's not how I think about it. Functions are great, but when I hear function I think C functions, which are tiny little instructions for tiny little machines and don't make any sense in a dependently-typed world. So instead, when I see the arrow, I think of it as a way of telling the type checker this fact: wherever you see the string "succ n", assign it the type ℕ but ONLY IF "n" is also of type ℕ. Think of the arrow as the lambda abstractor, and the space as the lambda applicator. Maybe that helps a little; maybe it hurts a lot. We plunge forward! _+_ : ℕ → ℕ → ℕ zero + n = n (succ n) + m = succ (n + m) More substitution rules. Whenever you see zero + n, the typechecker is allowed to replace it with n. Whenever you see (succ n) + m, it's allowed to replace it with succ (n + m). Allowed, but not required: the typechecker should only use these rules if it needs help typechecking a string it doesn't recognize. We would now like describe even numbers in Agda. Could we just define data even : Set? And thus give Set its second element? No! Because evenness is a proposition! It _depends_ on our other type ℕ, which is where we get our fancy dependently-typed programming from. We really want to say this: data even 0 : Set data even 2 : Set data even 4 : Set But that would be tedious. So instead we say data even : ℕ → Set If the arrow means substitution, like before, we can think about it like this: wherever we see the string "even n", assign it the type Set (a.k.a. let it be a valid type) but ONLY IF "n" has type ℕ. Is that true for any n? Nope. If it were, we would write data even : ℕ → Set where even_everything_is_goddamn_even : (n : ℕ) → even n Instead, we first assume that "even n" is true for no n at all. That's right: a function with an empty domain. We fill in the domain gradually. data even : ℕ → Set where even_zero : even zero even_succ : (n : ℕ) → even n → even (succ (succ n)) First, even zero means that "even zero" is a member of Set. zero is a natural number, so this typechecks. Second, suppose you have n : ℕ. And suppose even n typechecks. Then even (succ (succ n)) also typechecks. It's simply another form of induction, although slightly trickier because we're trying to fill out a proposition. Anyway. Hope that helps more than it confuses. I think Learn You An Agda makes it more confusing that it really is by not explaining Set and by using that weird postfix notation. Set is just Haskell's asterisk kind "*" if you know Haskell; otherwise it's pretty hard to grok for a while. You should also check out Benjamin Pierce's textbook on Coq programming, which expands on a lot of these details. (Coq and Agda and Idris are all pretty much are built on the same ideas.) http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

tomwilde 12y ago

If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them? In case the compiler can do that conversion: is it is programmed to do that for some subset of numeric types or can it infer an optimal binary representation of a value somehow? On the other hand, if they really were represented as lists then I presume this language is intended as purely academic work and has no application in a production environment. Am I wrong?

Dewie 12y ago
It's a proof assistant. Not really something you use for number crunching, industry or not.
- eli_gottlieb 12y ago
  But a proof assistant for numerical programming would be extremely useful.
chriswarbo 12y ago
> If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them? I don't think so, but Natural numbers can't be represented as two's-complement "integers"; neither can Integers. There are many ways to encode such numbers if you really want; the easiest are probably "Fin (2^32)" for a type with 2^32 members (easy to convert to/from unary Naturals), or "Vect 32 Bool" for a list of 32 Booleans (easy to do bitwise stuff). You'd need to decide how to truncate the Naturals though; do you take min(x, 2^32 - 1)? Do you take x % 2 ^ 32? Also, note that "S (S (S (S Z)))" isn't really a list; to turn it into a list we'd have to associate some trivial data with each constructor, eg. [NULL, NULL, NULL, NULL].
hesselink 12y ago
I always thought the statement {-# BUILTIN NATURAL ℕ #-} binds the inductive definition of ℕ to an efficient implementation. However, googling now I can find no confirmation of this. Does anyone know more?

alphonse23 12y ago

I posted this on lobste.rs and somebody stole my link.... Hackernews always gets so much more comments.

bkirwi 12y ago
Not guilty! I picked this one up on Twitter this afternoon, but it's possible the lineage traces back to your lobste.rs post. (I have no lobste.rs account, though not for lack of interest -- while sparse, the comments there seem to be of very high quality.)
d2xdy2 12y ago
When are they going to open registration back up on there?

agumonkey 12y ago

First time I read about 'mixfix' operators, one less thing I'll have to invent I guess. https://www.google.fr/search?q=mixfix+notation https://www.google.fr/search?q=mixfix+notation

olderwannalear 12y ago

My thanks OVERFLOWS. For those who are 'older but not quite Learn U Agda vs 'wiser strategies' HELPFUL. Think eric raymond and too bad that perl is just another dead language -- your wisdom though as recompense. When you are older, it becomes EASIER for crunchfit and yes, it sometimes becomes harder to exercise to point of vomit - "ad nauseum' in Latin, but the pain is much easier. Don't you do three hundred (300) pushups a day? So, the routine is simple. Get stuck running Haskell (another bump on the road to the true language of Coq) - go ahead and flame - do the pushups. Then laugh cause it releaxes and then refrshed back to AGDA. PS. Engineering school was arduous and graduate school. The personal private books/research were just hobbies and no I will not mention my name. Even the so-called Yourdon 'death marches' are just a bump on the road. It's worse than some females - over the period of a 'big city man.' - go ahead flame - Just take code from arxiv, run it in Haskell and Agda and there are only three explanations 1.)the programmer is stupdi - yup that's me 2.)scientific fraud - always possible 3.)the 'compiler' or the strange AMD CPU is fickle in a feminine way? 4.)the language paradigm is 'slightly broken.' 5.) all of the above Fair Warning and Serpents be Here. Haskell, Agda and even Coq are DEFINED as EXPERIMENTAL RESEARCH Languages. Of course, you can always go Python (which version?) and Javascript, which is the bubble gum and string that holds together the Internet.. along with BAsh shellshock. It this why they call it a bit of 'hacking'? PPS. learn to ride bicycle in big city and survived with most of my fingers intact.

eli_gottlieb 12y ago

Ok, that's neat. Is there a proof checker and an editor/IDE other than Emacs' Agda mode? Because I'm probably going to stick with Coq for its tooling.

frontsideair 12y ago

I always wondered about dependent types. Even though it was a little bit too technical for me, at least I have some idea about what it really is. By the way, Z notation rocks.

akkartik 12y ago

It lost me at this point: Type the following into an emacs buffer, and then type C-c C-l (use \_1 to type the subscript symbol ₁): proof₁ : suc (suc (suc (suc zero))) even proof₁ = ? On my newly created emacs setup from the earlier instructions, it's not clear what "type into an emacs buffer" means. Do I create a new file with C-x C-f? Create a new buffer with C-x b? I tried both, and promptly lost agda-mode. I then tried restarting emacs and opening a new .agda file so I get agda mode. Loaded the earlier module and then tried loading this, and it didn't seem to know about suc in the context of this buffer/file. So now I'm lost.

sjolsen 12y ago
That should read, "Type the following into the Emacs buffer." You should have something like: module LearnYouAn where data ℕ : Set where zero : ℕ succ : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + m = m (succ n) + m = succ (n + m) data _even : ℕ → Set where ZERO : zero even STEP : ∀ n → n even → succ (succ n) even proof₁ : succ (succ (succ (succ (zero)))) even proof₁ = ?
- akkartik 12y ago
  Thanks! Can't believe I didn't think of that :/ What's the distinction between C-c C-space and C-c C-r? It looks like the former computes proof obligations for ?s, but what does the latter do? And why couldn't we use the latter in the first instance, to deduce the outermost STEP ? ? Edit: never mind, that did work.
  - sjolsen 12y ago
    > What's the distinction between C-c C-space and C-c C-r? Beats the hell out of me. Here's the docstring for agda2-give (bound to C-c C-SPC): Give to the goal at point the expression in it Here's the one for agda2-refine (C-c C-r): Refine the goal at point. If the goal contains an expression e, and some "suffix" of the type of e unifies with the goal type, then the goal is replaced by e applied to a suitable number of new goals. If the goal is empty, the goal type is a data type, and there is exactly one constructor which unifies with this type, then the goal is replaced by the constructor applied to a suitable number of new goals.