Ryan Ingram wrote:

Congratulations, you're halfway to reinventing ST! :)

Except that, AFAIK, ST doesn't provide the "hey you can store anything and retrieve it later" trick. ;-) I did however wonder if there wasn't some way I could use an extra phantom type to somehow "tag" which thread a key was generated in... but I couldn't figure out how to make it work.

Here's the "trick" [1]:

...

data Storage s x ... data Key s v ...

Now add the extra "s" parameter to all the functions that use Storage & Key.

...

run :: (forall s. Storage s x) -> x

Now you can't save keys between sessions; the type "s" isn't allowed to escape the "forall" on the left of the function arrow!

Ah, I see. It sounds so easy when you already know how... :-) BTW, does anybody know how rank-N types are different from existential types?

What ST doesn't provide is a delete operation, otherwise it the rest (but in a safe way). On Thu, Dec 11, 2008 at 9:04 PM, Tillmann Rendel wrote:

Andrew Coppin wrote:

...

Except that, AFAIK, ST doesn't provide the "hey you can store anything and retrieve it later" trick. ;-)

I would say that Data.STRef does exactly that.

Tillmann _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Thu, Dec 11, 2008 at 2:05 PM, Andrew Coppin wrote:

Tillmann Rendel wrote:

...

Andrew Coppin wrote:

...

Except that, AFAIK, ST doesn't provide the "hey you can store anything and retrieve it later" trick. ;-)

I would say that Data.STRef does exactly that.

That's true - but you can't transport those from place to play. (By design.)

If you could guarantee that the ID of a key is globally unique, even through different invocations of the monad (using eg. unsafePerformIO newUnique), then you could ensure type safety and allow transport of keys between different monads. However, if you did this, then your library would not be referentially transparent. Can you see how? Luke

On Thu, Dec 11, 2008 at 1:48 PM, Andrew Coppin wrote:

BTW, does anybody know how rank-N types are different from existential types?

You mean the Haskell extensions? ExistentialQuantification lets you define types such as, data SomeNum = forall a. Num a => SomeNum a RankNTypes lets you nest foralls arbitrarily deep in type signatures, callCC :: ((forall b. a -> m b) -> m a) -> m a -- this is rank-3 RankNTypes implies ExistentialQuantification (among others). -- Dave Menendez http://www.eyrie.org/~zednenem/

Am Sonntag, 14. Dezember 2008 00:00 schrieb Andrew Coppin:

David Menendez wrote:

...

On Thu, Dec 11, 2008 at 1:48 PM, Andrew Coppin

wrote:

...

BTW, does anybody know how rank-N types are different from existential types?

You mean the Haskell extensions?

ExistentialQuantification lets you define types such as,

data SomeNum = forall a. Num a => SomeNum a

RankNTypes lets you nest foralls arbitrarily deep in type signatures,

callCC :: ((forall b. a -> m b) -> m a) -> m a -- this is rank-3

RankNTypes implies ExistentialQuantification (among others).

So how is

foo :: ((forall b. a -> m b) -> m a) -> m a

Here, the argument of foo's argument must be a polymorphic function, capable of returning an (m b) whatever b is.

different from

bar :: forall b. ((a -> m b) -> m a) -> m a

Here, the argument of bar's argument can have any monomorphic type (a -> m b)

then?

On Sat, Dec 13, 2008 at 6:00 PM, Andrew Coppin wrote:

David Menendez wrote:

...

On Thu, Dec 11, 2008 at 1:48 PM, Andrew Coppin wrote:

...

BTW, does anybody know how rank-N types are different from existential types?

You mean the Haskell extensions?

ExistentialQuantification lets you define types such as,

data SomeNum = forall a. Num a => SomeNum a

RankNTypes lets you nest foralls arbitrarily deep in type signatures,

callCC :: ((forall b. a -> m b) -> m a) -> m a -- this is rank-3

RankNTypes implies ExistentialQuantification (among others).

So how is

foo :: ((forall b. a -> m b) -> m a) -> m a

different from

bar :: forall b. ((a -> m b) -> m a) -> m a

then?

Daniel Fischer already gave the short answer, I'll try explaining why someone might *want* a rank-3 signature for callCC. It involves a continuation monad, but hopefully nothing headache-inducing. The type for callCC in Control.Monad.Cont.Class is, callCC :: forall m a b. (MonadCont m) => ((a -> m b) -> m b) -> m b You can use callCC to do very complicated things, but you can also use it as a simple short-cut escape, like the way "return" works in C. foo = callCC (\exit -> do ... x <- if something then return 'a' else exit False ... return True) The type of exit is Bool -> m Char, which is fine in this example, but it means that we can only use exit to escape from computations that are producing characters. For example, we cannot write, bar = callCC (\exit -> do ... x <- if something then return 'a' else exit False y <- if something then return 42 else exit False ... return True) Because exit would need to have the type Bool -> m Char the first time and Bool -> m Int the second time. But, if callCC had a rank-3 type, callCC :: forall m a. (MonadCont m) => ((forall b. a -> m b) -> m a) -> m a then exit would have the type "forall b. Bool -> m b", and bar would compile just fine. -- Dave Menendez http://www.eyrie.org/~zednenem/

On Fri, Dec 12, 2008 at 2:48 AM, Martijn van Steenbergen wrote:

I've worried about this but I couldn't find a good code example of when this goes wrong. Can you? Without using any of the unsafeXxx functions, of course.

Maybe I should build my monad on top of the ST monad if that makes things safer.

[1] http://hackage.haskell.org/packages/archive/Yogurt/0.2/doc/html/Network-Yogu...

Here's a simple example: runMud :: Mud a -> a runMud = flip evalState emptyMud main = do let v = runMud (mkVar "hello") let crash = runMud $ do v2 <- mkVar True -- v2 :: Var Bool res <- readVar v -- v :: Var String return res print crash -- boom! Both v2 and v are the same variable index (0), but different types. Since there's nothing preventing the variable from escaping from the first "runMud", we can import it into the second one where it fails. The key is that both use the same "initial state", so you have lost the uniqueness of variables. ST is safer, although you can make these systems just as safe with the phantom "state" type like ST does. It's also faster; variables turn directly into pointer references, instead of traversing an IntMap. But it gets kind of annoying writing all the extra "s" on your type signatures. -- ryan