[Agda] result code explosion
Serge D. Mechveliani
mechvel at botik.ru
Thu Apr 4 16:49:59 CEST 2013
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,
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.
More information about the Agda