[Agda] JS compiler - normalization

[Alan Jeffrey]

Hi all,

That would be my code then...

The JS compiler does indeed normalize types (not expressions) during 
compilation. The reason why is to perform singleton analysis: if a type 
T can be determined to only have one value v, then any expression of 
type T is replaced at compile time by v. For example, types of the form 
T1 -> ... -> Tn -> Set l, are singleton types containing the value 
lambda x1 ... lambda xn . *.

The main reason for performing singleton analysis is to stop the 
generated code from performing type-level computation at run-time, which 
would otherwise be wasted effort. The way this is implemented right now 
is a simplistic syntactic check on the normalized types.

I've not tried running the standard library through the JS compiler, and 
I'm not surprised it blows up. For JS development I've been using a 
stripped-down collection of data bindings, at:

   https://github.com/agda/agda-frp-js

A.

On 08/30/2012 08:22 AM, Andreas Abel wrote:
> Hello Stanislav,
>
> On you questions:
>
> 1. I do not know the JS compiler and I do not know why it normalizes.
> Normalization can be a bad idea, e.g., consider this Haskell program:
>
> mylist = [1..100000000000]
>
> main = do
> n <- parse first command line argument
> print (take n mylist)
>
> Normalizing mylist would probably make the compiler run out of mem.
>
> 2. Normalization is guaranteed to terminate. However, it might produce
> insanely large normal forms (see above and issue 415):
>
> http://code.google.com/p/agda/issues/detail?id=415
>
> Maybe try to switch off normalization in the JS compiler and see what
> happens...
>
> Cheers,
> Andreas
>
> On 30.08.12 2:43 PM, Станислав Черничкин wrote:
>> Howdy, humans!
>>
>> I'm trying to solve following issue:
>> http://code.google.com/p/agda/issues/detail?id=684. Short story: Agda
>> runs out of 1 GB when attempting to compile standard library with JS
>> compiler. I'm using head revision (version 2.3.1 so far) from the
>> darcs repository. The problem occurred while compiling
>> Data.Bool.Properties module, several other modules can be compiled
>> normally. MAlonzo compiler is able to compile whole library with
>> relatively low memory footprint (less than 200 MB), I faced problem
>> with JS compiler, I have not tried Epic.
>>
>> I investigated problem a bit and found, that bad things happening then
>> JS compiler tries to normalize term
>> Data.Bool.Properties.XorRingSolver._.⟦_⟧↓ (Compiler.hs:239). The
>> normalization does not seems to terminate or, at least, takes enormous
>> amount of memory (more than 1GB). I'm new to Agda, so I appreciate any
>> help/link from more experienced colleagues in solving this issue and
>> answering my questions:
>>
>> 1. What JS compiler uses normalization for? Why MAlonzo does not call
>> normalise function?
>> 2. Does normalization guaranteed to terminate? Can it produce enormous
>> structure from relatively short input? Is
>> Data.Bool.Properties.XorRingSolver such case and how it can be
>> diagnosed?
>> 3. Has someone tried to compile standard library with JS compiler
>> and/or faced similar issue?
>>
>> Thanks.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>