News for hackers. Stuff that matters.

A comment on Imperative Haskell. Parent comment

Re:Imperative Haskell by mietek on Wednesday May 31, 2017 @07:49AM (#14451734)
> 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://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8d...

http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf

[ Parent | on HN ]
Re:Imperative Haskell by cousin_it on Wednesday May 31, 2017 @08:14AM (#14451841)
AFAIK the Agda implementations use a closed universe of types and cannot be translated to an implementation of runST in Haskell which doesn't have that restriction. Please correct me if I'm wrong. From a quick reading I can't tell if the new paper makes progress on that front, what do you think?
[ Parent | on HN ]