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.<div>
<br></div><div>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 <font face="'courier new', monospace">f ∷ replicate f ⊛ xs </font>which can be really confusing in a larger term.</div>
<div><br><div class="gmail_quote">On Mon, May 7, 2012 at 3:33 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 07.05.12 7:06 PM, Daniel Peebles wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
*Come up with a neat solution to control depth of evaluation locally*<div class="im"><br>
<br>
See <a href="http://code.google.com/p/agda/issues/detail?id=433" target="_blank">http://code.google.com/p/agda/<u></u>issues/detail?id=433</a><br>
<br>
I see this mostly as an ease-of-use feature, but it might also help<br>
performance. Basically, often you really don't want terms to normalize<br>
fully in your goals or context. Some of my proofs have goals whose<br>
normal forms are thousands (literally) of lines long, so the goal output<br>
becomes effectively unusable.<br>
<br>
Most of the time, I want to work at a higher level of abstraction than<br>
individual recursively defined functions, and I've already proved simple<br>
lemmas about them. In those cases, I don't want simple definitions to<br>
normalize past a certain point, and want to prove things about the<br>
higher-level expressions.<br>
<br>
For example, when I'm writing simple proofs about the algebraic<br>
properties of operations on the naturals, I might want my definitions to<br>
normalize, but other times I might not. For example, (1 + x) + ((1 + y)<br>
* (1 + z)) will normalize to the horrible suc (x + suc (z + y * suc z)).<br>
If I have a proof about the original form, it takes a lot of squinting<br>
to realize that the normal form applies to it.<br>
</div></blockquote>
<br>
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.<br>
<br>
Unfortunately, that would still destroy your beautiful 1 + x.<br>
<br>
However, Data.List's<br>
<br>
any p xs<br>
<br>
would not be unfolded to<br>
<br>
foldr _v_ false (map p xs).<br>
<br>
Which would already be something.<br>
<br>
Cheers,<br>
Andreas<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div>