[Agda] evaluation in compilation

[Andreas Abel]

On 03.10.12 4:57 PM, Serge D. Mechveliani wrote:
> On Wed, Oct 03, 2012 at 01:47:08AM +0200, Andreas Abel wrote:
>> When I try to load your example, I get a "stack overflow".  So it is not
>> a problem of the compiler, but already type checking fails.
>
> Does type check constitute an essential part of compilation?

Agda first type-checks, which sometimes has to do computation and 
normalization.

Then Agda compiles e.g. to Haskell, which does not involve any extra 
normalization.

>> I found the problem:
>>
>>> zs = merge xs ys
>> -- this works
>> bla : List ??? ??? List ???
>> bla [] = []
>> bla (z ??? zs') =  z ??? (last $ fromL z zs') ??? []
>>
>> hl = bla zs
>
>
> But  bla zs =  bla (merge xs ys),
>
> and  merge  and  bla  have explicit evaluation rules, and there are
> explicit rules for constructing  xs and ys.
> So,  bla zs  will be normalized at compilation time, as soon as the
> compiler sees all these rules (clauses).
> Why there is a difference in normalization in `with' and in the two
> patterns for  bla ?
> Or may be, I do not know what is normalization in Agda.

There is no normalization going on in this case.  Agda does not fully 
normalize stuff before compilation, even if it could do.  But it is not 
always to the advantage.

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/