<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&#39;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&#39;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 &quot;master&quot; 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&#39;m refactoring the code gradually, my next target is interaction points.  I&#39;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>