[Agda] Bounties for Agda features

[Daniel Peebles]

Hi all,

I posted these bounties for Agda features (effectively an attempt to
prioritize work on features that I care about) on Google+ and on Twitter,
but this seems like the best place to post them, to get the most exposure
to people who know the most about Agda.

Please let me know if you see any issues in how I've set this up. Also, if
you think you know someone who might be interested in working on any of
these, pointing them to http://bitbounties.org/agda should work.

Thanks,
Daniel


-----------------------------------------------------------------------------------------------------------------------------------

These bounties will be paid to anyone who manages to get patches for the
listed features into the Agda repository. As with any other open-source
venture, the code should be good and the project maintainers shouldn't be
burdened by your work, beyond basic merging efforts. That is, please don't
pester Ulf, Nils, or Andreas too much for help. The last thing I want to do
with the bounties is give them more work. And if you are Ulf, Nils, or
Andreas, you're still eligible for the bounties, of course! I also welcome
collaboration between people, in which case I will split the bounty as the
participants see fit.

Although you should not annoy the maintainers, I do welcome public
discussion on the mailing list about how the features below should be
implemented. It'd be horrible if you went off and implemented the most
awesome approach to the problems below, and then it turned out a maintainer
didn't like the approach, or was already implementing it differently.
Basically, the bounties should not affect your standards of code quality
and team work.

As far as standards are concerned, I leave the judgment up to the
maintainers. If they merge your code into the main repository, you get my
coins and eternal gratitude. If they don't, I hope you can work things out
so that they do :)

And if you really hate bitcoins and think they're a pyramid
scheme/scam/whatever other criticisms have been thrown at them, I'd be
willing to give you the equivalent market value (as judged by the MtGox
exchange rate) of the coins at the time of payment with Dwolla or PayPal.
I'd really prefer Dwolla though; not really a fan of PayPal.

Of course, if other people would like to add money to the pots for these
bounties or others, I'll happily post the updates here.

If you'd like to contact me about this stuff, I'm copumpkin on freenode and
twitter, or Daniel Peebles on Google+ (and most other places :P).


*Share terms in the normalizer / compile-time evaluator*

As we all know, large Agda projects quickly get bogged down by excessive
resource consumption. A lot of the bad performance can be attributed to the
almost complete lack of sharing in in-memory Agda terms, which means both a
blow-up in RAM usage by storing many identical copies of the same term, and
a blow-up in processing time computing them.

There are a couple of approaches to improving this, from what I've heard.
One is hash-consing, where you keep a global stash of all terms and
subterms and make to grab the canonical one every time you construct a new
one. This should lead to perfect sharing, but might be painful to implement
and could slow things down with all the hashing of complex structures
involved. Another approach is to implement something more closely
resembling Haskell's call-by-need evaluator.

Bounty: 100 BTC


*Only reload changed parts of the source in the interactive environment*

I'd prefer this to be implemented generally, as I think the interaction
machinery is trying to move away from strict emacs-specific behavior.
Basically, C-c C-l currently always reloads the entire file when you run
it, even if you've only changed a tiny piece of it.

I can think of two approaches to this, but I don't really care how it's
done as long as it works. One approach is to parse and then run some sort
of a clever diff on the parse tree before typechecking. The other is to run
a textual diff and do something similar. The latter approach would likely
work at the declaration level. Given the weird non-local behavior of
constraints (I think this has decreased now, but back in the day you could
write a really specific proof about a function and leave the function to be
inferred by the constraints solver), determining how much would change
given an AST-level change might be tricky.

Bounty: 100 BTC


*Come up with a neat solution to control depth of evaluation locally*

See http://code.google.com/p/agda/issues/detail?id=433

I see this mostly as an ease-of-use feature, but it might also help
performance. Basically, often you really don't want terms to normalize
fully in your goals or context. Some of my proofs have goals whose normal
forms are thousands (literally) of lines long, so the goal output becomes
effectively unusable.

Most of the time, I want to work at a higher level of abstraction than
individual recursively defined functions, and I've already proved simple
lemmas about them. In those cases, I don't want simple definitions to
normalize past a certain point, and want to prove things about the
higher-level expressions.

For example, when I'm writing simple proofs about the algebraic properties
of operations on the naturals, I might want my definitions to normalize,
but other times I might not. For example, (1 + x) + ((1 + y) * (1 + z))
will normalize to the horrible suc (x + suc (z + y * suc z)). If I have a
proof about the original form, it takes a lot of squinting to realize that
the normal form applies to it.

Bounty: 50 BTC

[Andreas Abel]

Post by Daniel Peebles
*Come up with a neat solution to control depth of evaluation locally*
See http://code.google.com/p/agda/issues/detail?id=433
I see this mostly as an ease-of-use feature, but it might also help
performance. Basically, often you really don't want terms to normalize
fully in your goals or context. Some of my proofs have goals whose
normal forms are thousands (literally) of lines long, so the goal output
becomes effectively unusable.
Most of the time, I want to work at a higher level of abstraction than
individual recursively defined functions, and I've already proved simple
lemmas about them. In those cases, I don't want simple definitions to
normalize past a certain point, and want to prove things about the
higher-level expressions.
For example, when I'm writing simple proofs about the algebraic
properties of operations on the naturals, I might want my definitions to
normalize, but other times I might not. For example, (1 + x) + ((1 + y)
* (1 + z)) will normalize to the horrible suc (x + suc (z + y * suc z)).
If I have a proof about the original form, it takes a lot of squinting
to realize that the normal form applies to it.

Well, a simple heuristics would be to only unfold definitions when
making progress, where progress means that a constructor-pattern matched
and an equation fired.

Unfortunately, that would still destroy your beautiful 1 + x.

However, Data.List's

any p xs

would not be unfolded to

foldr _v_ false (map p xs).

Which would already be something.

Cheers,
Andreas

[Daniel Peebles]

That could be a good start, but ultimately it'd be nice to have better
user-specified control over it, somehow. In the categories library there
are pretty much no constructors or pattern matching anywhere but many
definitions expand to more complicated definitions that will often obscure
the proofs (and probably increase memory usage). We currently selectively
throw things behind abstract barriers, along with proofs that the abstract
terms are equal to their definitions, but that's really tedious and far
from ideal.

One of the more annoying constructor-y situations I've come across is when
I use the standard library map function on a term xs (that I have not
pattern matched on) whose length is (suc ...). Then I end up with the
replicate in the definition of map producing an extra element like f ∷
replicate f ⊛ xs which can be really confusing in a larger term.

Post by Daniel Peebles
*Come up with a neat solution to control depth of evaluation locally*
See http://code.google.com/p/agda/**issues/detail?id=433<http://code.google.com/p/agda/issues/detail?id=433>
I see this mostly as an ease-of-use feature, but it might also help
performance. Basically, often you really don't want terms to normalize
fully in your goals or context. Some of my proofs have goals whose
normal forms are thousands (literally) of lines long, so the goal output
becomes effectively unusable.
Most of the time, I want to work at a higher level of abstraction than
individual recursively defined functions, and I've already proved simple
lemmas about them. In those cases, I don't want simple definitions to
normalize past a certain point, and want to prove things about the
higher-level expressions.
For example, when I'm writing simple proofs about the algebraic
properties of operations on the naturals, I might want my definitions to
normalize, but other times I might not. For example, (1 + x) + ((1 + y)
* (1 + z)) will normalize to the horrible suc (x + suc (z + y * suc z)).
If I have a proof about the original form, it takes a lot of squinting
to realize that the normal form applies to it.

Well, a simple heuristics would be to only unfold definitions when making
progress, where progress means that a constructor-pattern matched and an
equation fired.
Unfortunately, that would still destroy your beautiful 1 + x.
However, Data.List's
any p xs
would not be unfolded to
foldr _v_ false (map p xs).
Which would already be something.
Cheers,
Andreas
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>

[Peter Hancock]

It seems to me this dream of selecting the "best" presentation of
something like a type in the current context is fantasy, and would amount to
Super Cow Powers or mind-reading or solving the halting problem.

But it is a very enticing fantasy, as any one will agree who has
spent time massaging pieces of text spat out by Agda into an intelligible form.
This seems to be mostly introducing "beta-expansions" and
local definitions, or (re-)factoring in some sense.

Some crude control over how the same thing is presented in different contexts
might be worthwhile if it cost next to nothing.

A system I used long ago called alfa
by Thomas Hallgren used to offer some control of this kind for a primeval version of agda.
Exaggerating slightly, you could ask to see your type-expression written in latin or punched-card
notation, using code contributed by Aarne Ranta.

Peter Hancock

[Thomas Hallgren]

Alfa offered a lot of control over how terms were presented, see

http://www.cse.chalmers.se/~hallgren/Alfa/Tutorial/GFplugin.html
http://www.cse.chalmers.se/~hallgren/Papers/lpar2000.ps.gz

http://www.cse.chalmers.se/~hallgren/Alfa/userguide.html#layout
http://www.cse.chalmers.se/~hallgren/Alfa/Tutorial/ndstyle.html

But this is orthogonal to how you control how far terms are unfolded...

Thomas H

Post by Peter Hancock
A system I used long ago called alfa
by Thomas Hallgren used to offer some control of this kind for a primeval version of agda.
Exaggerating slightly, you could ask to see your type-expression written in
latin or punched-card
notation, using code contributed by Aarne Ranta.
Peter Hancock

[Andreas Abel]

Post by Daniel Peebles
That could be a good start, but ultimately it'd be nice to have
better user-specified control over it, somehow.

Ok, do you have an idea how that should look like? Coq, e.g., has the
"unfold" tactic (or was it "expand", cannot remember).

In Agda, an "unfold" has no significance and would leave no trace in the
file, it would be a temporary change of the proof state, maybe.

Post by Daniel Peebles
In the categories library there are pretty much no constructors or
pattern matching anywhere but many definitions expand to more
complicated definitions that will often

But would that not be prevented by my proposal? If no pattern matching
fires, expansion does not bring progress, so it does not happen...

Post by Daniel Peebles
obscure the proofs (and probably increase memory usage). We currently
selectively throw things behind abstract barriers, along with proofs
that the abstract terms are equal to their definitions, but that's
really tedious and far from ideal.

:-(

Post by Daniel Peebles
One of the more annoying constructor-y situations I've come across is
when I use the standard library map function on a term xs (that I
have not pattern matched on) whose length is (suc ...). Then I end up
with the replicate in the definition of map producing an extra
element like f ∷ replicate f ⊛ xs which can be really confusing in a
larger term.

Certainly, you would not want such partial unfoldings, exposing the
concrete definition of map.

It would be nice if the implementation of a function could be hidden
behind a more abstract reduction interface, like

map f [] --> []
map f (x :: xs) --> f x :: map f xs

even if that is not the definition of map.

In general, the state of rewrite rules in Agda is unsatisfactory. They
cannot be part of an interface, you can only specify them as
propositional equations. However, these do not fire during reduction,
which makes abstract program development tedious, if not unfeasible.

With rewrite rules as a primitive, we could also have very handy
simplification rules like

x + 0 --> x

There is tons of literature on rewriting in type theory which we have
not made use of. Of course, care is called for, since rewriting easily
destroys termination and confluence.

Cheers,
Andreas

Post by Daniel Peebles
*Come up with a neat solution to control depth of evaluation
locally*
See http://code.google.com/p/agda/__issues/detail?id=433
<http://code.google.com/p/agda/issues/detail?id=433>
I see this mostly as an ease-of-use feature, but it might also help
performance. Basically, often you really don't want terms to
normalize fully in your goals or context. Some of my proofs have
goals whose normal forms are thousands (literally) of lines long, so
the goal output becomes effectively unusable.
Most of the time, I want to work at a higher level of abstraction
than individual recursively defined functions, and I've already
proved simple lemmas about them. In those cases, I don't want simple
definitions to normalize past a certain point, and want to prove
things about the higher-level expressions.
For example, when I'm writing simple proofs about the algebraic
properties of operations on the naturals, I might want my definitions
to normalize, but other times I might not. For example, (1 + x) + ((1
+ y) * (1 + z)) will normalize to the horrible suc (x + suc (z + y *
suc z)). If I have a proof about the original form, it takes a lot
of squinting to realize that the normal form applies to it.
Well, a simple heuristics would be to only unfold definitions when
making progress, where progress means that a constructor-pattern
matched and an equation fired.
Unfortunately, that would still destroy your beautiful 1 + x.
However, Data.List's
any p xs
would not be unfolded to
foldr _v_ false (map p xs).
Which would already be something.

[Nils Anders Danielsson]

Post by Andreas Abel
Well, a simple heuristics would be to only unfold definitions when
making progress, where progress means that a constructor-pattern
matched and an equation fired.
Unfortunately, that would still destroy your beautiful 1 + x.
However, Data.List's
any p xs
would not be unfolded to
foldr _v_ false (map p xs).
Which would already be something.

You can control the amount of unfolding in the output:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations

If you use the "without normalising" variants, then things are often
less unfolded.

Tomas Hallgren mentioned to me that it can be a problem that
meta-variables are instantiated with unfolded terms. Perhaps we should
store two copies of terms, one with minimal unfolding and one which
records the unfolding that we have already performed (to avoid
recomputing things).

[Nils Anders Danielsson]

Post by Daniel Peebles
*Only reload changed parts of the source in the interactive environment*
I'd prefer this to be implemented generally, as I think the
interaction machinery is trying to move away from strict
emacs-specific behavior. Basically, C-c C-l currently always reloads
the entire file when you run it, even if you've only changed a tiny
piece of it.
I can think of two approaches to this, but I don't really care how
it's done as long as it works. One approach is to parse and then run
some sort of a clever diff on the parse tree before typechecking. The
other is to run a textual diff and do something similar. The latter
approach would likely work at the declaration level. Given the weird
non-local behavior of constraints (I think this has decreased now, but
back in the day you could write a really specific proof about a
function and leave the function to be inferred by the constraints
solver), determining how much would change given an AST-level change
might be tricky.

We've had something like this for a while now (--caching). I think
Andrea Vezzosi was the main implementor of this feature.

Post by Daniel Peebles
Bounty: 100 BTC

:)