[Haskell-cafe] Re: ANNOUNCE: pqueue-mtl, stateful-mtl

[Ryan Ingram]

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
<ccshan at post.harvard.edu> wrote:
> Ryan Ingram <ryani.spam at gmail.com> wrote in article <2f9b2d30902151615n1e8e25e8ubbee20d93c8ecd32 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>