[Agda] evaluation in compilation

Serge D. Mechveliani mechvel at botik.ru
Fri Oct 5 10:26:35 CEST 2012

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 
In both the cases normalization is before run time, and it is expensive
due to applying call by name.
And this all is a matter of MAlonzo, because I use MAlonzo, and these
effects happen before producing the Haskell code.

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.



More information about the Agda mailing list