Hmm, that's a really good question now that you mention it. So, the implementation given is trivially *not* type-safe; eventually the Int index will wrap around and reuse indices at the potentially wrong type.
But lets say you replaced IntMap with Map Integer, to avoid this problem. A simple property: STTRefs cannot escape to another STT session. Proof: See SPJ's original ST paper. This is actually kind of useful on its own, because you can nest STTs over each other to provide something like regions. Then it comes down to, within a session, is there some way for an STTRef to "mingle" and break the type-safety rule. I can think of two potential ways this might happen. First, if the underlying monad is something like List or Logic, there may be a way for STTRefs to move between otherwise unrelated branches of the computation. Second, if the underlying monad is something like Cont, there may be a way for an STTRef to get transmitted "back in time" via a continuation to a point where it hadn't been allocated yet. So if there is a counterexample I expect it to come down to one of those two cases. -- ryan On Thu, Feb 26, 2009 at 11:22 PM, Chung-chieh Shan <ccs...@post.harvard.edu> wrote: > Ryan Ingram <ryani.s...@gmail.com> wrote in article > <2f9b2d30902151615n1e8e25e8ubbee20d93c8ec...@mail.gmail.com> in > gmane.comp.lang.haskell.cafe: >> You can roll your own pure STT monad, at the cost of performance: > > Do you (or anyone else) know how to prove this STT implementation > type-safe? It seems to be safe but I'm not sure how to prove it. > > -- > Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig > A mathematician is a device for turning coffee into theorems. > Paul Erdos (1913-1996) > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
