[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Thu, Oct 04, 2012 at 10:56:44PM +0200, Andreas Abel wrote:
>
>
> 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 Nat -> List Nat
>>> bla [] = []
>>> bla (z :: zs') =  z :: (last $ fromL z zs') ??? []
>>>
>>> hl = bla zs

(I replaced math symbols -- Sergei).

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


So, with `with' in this example, normalization happens at type-check.
And with `bla'  is happens after type-check and still in the compilation 
time.
Right?
In both the cases normalization is before run time, and it is expensive
due to applying call by name.
Right?
And this all is a matter of MAlonzo, because I use MAlonzo, and these
effects happen before producing the Haskell code.
Right?

Anyway this particular example is done all right -- by moving the counter
constant initiation to a separate   module Constants.

I do not know, so far, whether I shall face in future the question of a 
too early normalization.

Regards,

------
Sergei