[Agda] result code explosion

[Serge D. Mechveliani]

On Thu, Apr 04, 2013 at 03:35:39PM +0200, Nils Anders Danielsson wrote:
> On 2013-04-02 14:45, Serge D. Mechveliani wrote:
> >400 lines of Agda  have converted to  23413 lines of the Haskell code.
> 
> Some potential reasons:
> 
> * Implicit arguments are made explicit.
> 
> * Things that could be shared (via let, say) aren't.
> 
> * Terms are normalised.
> 
> * Things that could be erased aren't.
> 

This code size ratio of about 60 may be in reality smaller, may be, say, 
15.
Because an Agda code seems to have more information density (on average) 
than the Haskell code. This is, for example, due to the meaning of type 
indices, and such, the relations between indices are kept by Agda.

Regards,

------
Sergei