[Agda] Refactoring typechecking monads

[Ulf Norell]

>
> [tech]: TCM is using IORef to hold the states.  Is IORef significantly
> faster than StateT or other equivalent?  If references are really superior,
> how about the ST monad?
>

I don't remember the exact numbers, since it was a while since I changed
it, but I do remember that it made a significant difference. However,
changing the monad implementation should be a very local change so I
encourage you to try it out. ST have a couple of problems: extra parameter
cluttering things up, and you can't do IO. We are using IO for debug
printing and for exceptions. Using ErrorT or similar for exceptions I'm
pretty sure would kill performance.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140620/c359b258/attachment.html