[Agda] Refactoring typechecking monads

[Ulf Norell]

Yeah standard library should do fine for that.

/ Ulf


On Mon, Jun 23, 2014 at 3:15 PM, Favonia <favonia at gmail.com> wrote:

> 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/20140624/645257c0/attachment.html