Re: [Haskell-cafe] Re: ANNOUNCE: pqueue-mtl, stateful-mtl
On Fri, Feb 27, 2009 at 11:10 PM, Ryan Ingram ryani.s...@gmail.com wrote: It's obvious that anything that accesses the STT constructor will potentially not be typesafe; the question I have is that whether you can construct something that isn't typesafe just via the use of runSTT lift. To my surprise, it turns out that you can. data Foo m a b = V a | K (Foo m a b - m b) test = do v - lift $ callCC $ \k - return (K k) case v of K k - do r1 - newSTTRef 'a' lift $ k (V r1) -- * V r1 - do r2 - newSTTRef (65 :: Int) return (r1,r2) The call to k in the marked line undoes the heap changes since the call to callCC, and we end up with r1 and r2 both pointing to the same cell. -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: ANNOUNCE: pqueue-mtl, stateful-mtl
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
Re: [Haskell-cafe] Re: ANNOUNCE: pqueue-mtl, stateful-mtl
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
Re: [Haskell-cafe] Re: ANNOUNCE: pqueue-mtl, stateful-mtl
I note that all of your broken issues revolve around calls that can't be written in terms of lift; that is, you need access to the STT constructor in order to create these problems. It's obvious that anything that accesses the STT constructor will potentially not be typesafe; the question I have is that whether you can construct something that isn't typesafe just via the use of runSTT lift. If you wanted to implement callCC directly (as opposed to lift . callCC) you would need to be extremely careful, as you noticed. -- ryan On Fri, Feb 27, 2009 at 2:27 PM, David Menendez d...@zednenem.com wrote: On Fri, Feb 27, 2009 at 1:28 PM, Ryan Ingram ryani.s...@gmail.com wrote: 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. I think promoting MonadPlus would be safe. The code for mplus will end up looking something like: mplus (STT a) (STT b) = STT (StateT (\heap - runStateT a heap `mplus` runStateT b heap)) so each branch is getting its own copy of the heap. The fancier logic stuff, like msplit, doesn't promote well through StateT, and isn't type-safe in STT For example: class (MonadPlus m) = ChoiceMonad m where msplit :: m a - m (Maybe (a, m a)) instance ChoiceMonad [] where msplit [] = [Nothing] msplit (x:xs) = [Just (x,xs)] There are at least two ways to promote msplit through StateT. The method I used in my library is, instance (ChoiceMonad m) = ChoiceMonad (StateT s m) where msplit m = StateT $ \s - msplit (runStateT m s) = return . maybe (Nothing, s) (\ ((a,s'),r) - (Just (a, StateT (\_ - r)), s')) If you promoted that instance through STT, it would no longer be safe. test = do Just (_, rest) - msplit $ mplus (return ()) (return ()) ref1 - newSTTRef 'a' rest ref2 - newSTTRef (65 :: Int) readSTTRef ref1 The call to rest effectively undoes the first call to newSTTRef, so that ref1 and ref2 end up referring to the same cell in the heap. I'm confident callCC and shift will cause similar problems. -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: ANNOUNCE: pqueue-mtl, stateful-mtl
Louis Wasserman wasserman.lo...@gmail.com wrote in article ab4284220902160801x51e6c3b6m3a7ee0698ac97...@mail.gmail.com in gmane.comp.lang.haskell.cafe: The point here is that a MonadST instance guarantees that the bottom monad is an ST -- and therefore single-threaded of necessity -- and grants any ST-based monad transformers on top of it access to its single state thread. This approach sounds like Fluet and Morrisett's monadic regions (ICFP 2004, JFP 2006), for which Oleg and I produced a easier-to-use implementation (Haskell 2008). You may find these papers helpful! http://ttic.uchicago.edu/~fluet/research/rgn-monad/ http://okmij.org/ftp/Haskell/regions.html#light-weight -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Attending a mathematics lecture is like walking through a thunderstorm at night. Most of the time you are lost, wet and miserable but at rare intervals there is a flash of lightening and the whole countryside is lit up. - Tom Koerner ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
