<div dir="ltr"><div><div><div><div><div><div><div>Dear Agda hackers,<br><br></div>One of my proposals at the last AIX was to refactor the typechecking monad (TCM). The goal is to clean up the current codebase so that a good Haskell API is immediately available. I'd like to break the typechecking monad into several monads, including but not limited to<br>
<br></div>1. scope checking<br></div>2. type checking<br><br></div>I'm still working on this, and I plan to refactor the program gradually. Some smaller patches have been merged into the codebase. I have one architectural question and one technical question though:<br>
<br></div>[arch]: If there should be a "master" monad invoking the type checking and scope checking, what should it be?<br><br></div>[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?<br>
</div><div><br></div><div>As I'm refactoring the code gradually, my next target is interaction points. I'd like to create a separate monad for scope checking and move interaction points from TCState to other places.<br>
</div><div><br></div>Thanks,<br>Favonia<br></div>