> You'd think that ST itself can be implemented in pure Haskell, maybe with the usual logarithmic slowdown. But unfortunately no one knows how to do it, and the

> You'd think that ST itself can be implemented in pure Haskell, maybe with the usual logarithmic slowdown. But unfortunately no one knows how to do it, and there's a strong suspicion that the (pure) type signature of runST has no pure implementation at all ... This information may be out of date. There are now at least two Agda formalisations of runST (by Andrea Vezzosi and András Kovács), and a paper by Timany et al. on the subject of runST has been submitted to ICFP'17. http://code.haskell.org/~Saizan/ST/ST.agda http://code.haskell.org/~Saizan/ST/ST.agda http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8dbd1dced6 http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8d... http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf