Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feedback Request: Using the CPS'd version of WriterT #1709

gallais opened this issue Oct 30, 2015 · 2 comments


None yet
3 participants
Copy link

commented Oct 30, 2015

Based on this thread, it looks like we could benefit from using the CPS'd
version of WriterT. I have added a Agda.Utils.CPSWriter module
implementing this behaviour and have ported all the usages of WriterT
in the codebase to this new definition.

This looks faster on my computer but the stats obtained when running
library-test have been varying quite a bit during the afternoon so I'm
not sure whether it's worth merging in master.

Any opinions? It's all sitting on this branch:


This comment has been minimized.

Copy link

commented Oct 30, 2015

I guess only a little of Agda's performance depends on WriterT, it is not used that much. However, I have no objections against merging this, except: Please do the refactoring on maint, and then merge it into master. Otherwise, we get more an more divergence between these branches.


This comment has been minimized.

Copy link

commented May 28, 2018

I'm guessing that this branch no longer merges cleanly with stable-2.5... Might still be worth updating it and doing some performance measurements though.

@UlfNorell UlfNorell added this to the 2.5.5 milestone May 28, 2018

@gallais gallais closed this Nov 14, 2018

@gallais gallais removed this from the 2.6.0 milestone Nov 14, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.