[Agda] Refactoring typechecking monads

Favonia favonia at gmail.com
Mon Jun 23 15:15:51 CEST 2014


What should be the test cases if I want to benchmark it?  The standard
library?  -Favonia


On Fri, Jun 20, 2014 at 10:52 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> [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/20140623/a1d550fc/attachment.html


More information about the Agda mailing list