[Agda] Re: Performance gains for normalization when dumping IO?

[James Deikun]

On Mon, 2012-04-30 at 09:49 +0200, Andreas Abel wrote:
> Evaluation does not need State or Error, so I started looking into 
> moving Reduce into a Reader monad.  However, I realized that TCM is a 
> combination of Reader and IO already:
> 
>    TCM = TCMT IO
>    TCMT m a = IORef State -> Env -> m a
> 
> I am not sure now wether moving out of IO will give noticable 
> performance gains.  In one of my experiments, I noticed a 10% speed up 
> for moving out of State and Error for evaluation, but I do not know 
> about IO...
> 
> Any experience/guesses?

I would expect that the performance gains would be limited by cases
where the signature is consulted or when simple things like
arity-raising might kill sharing (I don't know how good GHC is at
avoiding this for Reader).  At least it would require care in the
implementation of reduction to not inspect the signature unless it is
strictly necessary, so that as much computation can be shared as
possible.

Also to maximize asymptotic gains in performance, an unevaluated 'reduce
t' should when possible always be stored alongside any term t that may
need to be reduced in future.  (Or instead of this term, if it will
never be inspected without attempting reduction.)

On my own I am trying a different approach, but this one is also worth
trying for its relative simplicity and its low impact on the cases where
the typechecker already performs well.