[Agda] Performance issues and code structure.

[Nils Anders Danielsson]

On 2009-09-27 05:49, Dan Doel wrote:
> Loading it up using the command line 'agda' command reveals that it's
> causing a (haskell) stack overflow.

I run Agda using the following command-line which increases the maximum
stack size (40M), and introduces a maximum heap size (2G) to avoid
swapping:

  agda +RTS -M2G -K40M -RTS

In Emacs I have set haskell-ghci-program-args to '("+RTS" "-M2G" "-K40M"
"-RTS").

> Is it the equational reasoning that's so expensive?

Probably not, but maybe it exacerbates the problem. You could try
replacing all the inferable code with underscores.

The Agda typechecker normalises code before checking equality. If the
normalised terms are large, then equality checking can be slow. Note
that records are η-expanded, and that sharing is /not/ preserved by
Agda's current call-by-name evaluator. Furthermore I believe that
lambda-lifting is performed before type-checking, which means that a
module (record) header's telescope is prepended to every definition
inside the module, thus causing even more equality checking to be
performed.

> Someone also suggest in #agda on freenode that bundling proof terms into 
> records representing structures caused performance problems, and that's why 
> the Algebra modules in the standard library are structured the way they are. 

No, the Algebra modules are structured using "Pebble-style sharing" (see
Pollack's "Dependently Typed Records in Type Theory") because sharing by
equations seemed to be quite inconvenient in Agda.

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.