[Agda] Bounties for Agda features

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

On Mon, May 7, 2012 at 3:33 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> On 07.05.12 7:06 PM, Daniel Peebles wrote:
>
>> *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
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120508/a39b3dc5/attachment.html