Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Learn You an Agda

williamdemeo.github.io

Post reply on HN
Print view View original

41–50 of 72 posts

Re: Learn You an Agda

#41

Post by shadytrees »

gosub wrote: post #13

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?

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

Re: Learn You an Agda

#43

Post by art-w »

pron wrote: post #40
chriswarbo wrote: post #34

Earlier quoted context omitted.

> 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. > At the end of the day, programs are written for their side effects The reason for such a focus on data transformation is that it's very easy to do in these purely functional languages (Agda included). It's so easy, in fact, that "…

But in your example the program doesn't represent the code itself but a program written in some new language. I said that current type systems are good for writing compilers, but not so good at describing their own behavior other than data transformations.

It's not reasonable to embed every possible language constructs, semantic and logic into a theorem prover. So the trick is to make the host generic enough to be able to embed your needs as a domain specific language: your critic becomes a library problem. Which implies that you only need to trust the host logic/implementation; and many people can work, collaborate and profit from the same core. Also, we kind of know how a generic logic can be done, but the domain specific logic are more controversial (because everyone needs are different.)

The fact that your DSL is represented as an immutable datastructure by the host is really not important. Any code you write is going to be turned into a datastructure at some point. The immutability should be read as "the context in which this result is valid has been made fully explicit", where "context" includes "things that mutate over time". You don't loose in expressivity, you just can't forget to handle special cases.

Re: Learn You an Agda

#44

Post by olderwannalear »

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.

Re: Learn You an Agda

#45

Post by platz »

pron wrote: post #9

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 (u…

Here Idris uses its effect system to verify correct usage of a protocol between a client and a server http://www.youtube.com/watch?v=vkIlW797JN8&t=53m35s

Re: Learn You an Agda

#46

Post by foobarbaz1234 »

pseudonom- wrote: post #16
pron wrote: post #9

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 (u…

It's not exactly what you're asking for but Ur/Web puts an expressive type system to some slightly unusual ends: http://www.impredicative.com/ur/ .

Keep also in mind, that it is ultra-fast (http://www.techempower.com/benchmarks/#section=data-r9&hw=pe...).

Re: Learn You an Agda

#47

Post by hesselink »

tomwilde wrote: post #26

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 we…

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?

Re: Learn You an Agda

#48

Post by pron »

art-w wrote: post #43
pron wrote: post #40

Earlier quoted context omitted.

But in your example the program doesn't represent the code itself but a program written in some new language. I said that current type systems are good for writing compilers, but not so good at describing their own behavior other than data transformations.

It's not reasonable to embed every possible language constructs, semantic and logic into a theorem prover. So the trick is to make the host generic enough to be able to embed your needs as a domain specific language: your critic becomes a library problem. Which implies that you only need to trust the host logic/implementation; and many people can work, collaborate and profit from the same core. Also, we kind of know…

I think this is a type system limitation that every type describing side effects -- i.e. the core of every interesting program other than a compiler/interpreter -- can only be used in the context of a compiler/interpreter.

Checker (Java 8's pluggable intersection type-system framework) is able to do that (define side-effect types), but isn't a single general type system. I.e. you need to write a different type system for each property (of course, they can all work together). Maybe that's the only known way to do that. Searching for more general solutions, I've come up empty handed (the problem is well known, but the solutions are all in early stages of research).

The idea of such a type system needs to be something like: each function has a set of types associated with it, and a function's type interacts with the types of the functions it calls in some ways. So the most primitive example is, of course, checked exceptions, where the type of a function is a simple union of the types of its callees. But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.

Re: Learn You an Agda

#49

Post by mike_hearn »

ocharles wrote: post #11
mike_hearn wrote: post #4

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 a…

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 mat…

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.

Re: Learn You an Agda

#50

Post by eli_gottlieb »

Dewie wrote: post #30
tomwilde wrote: post #26

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 we…

It's a proof assistant. Not really something you use for number crunching, industry or not.

But a proof assistant for numerical programming would be extremely useful.
Post reply on HN