I wrote:

...

Prelude Control.Monad.ST> runST (return 42) 42 Prelude Control.Monad.ST> (runST . return) 42

<interactive>:1:9: Couldn't match expected type `forall s. ST s a' against inferred type `m a1'

Brian Hulley wrote:

Hazarding a guess, I suggest it *might* be due to the fact that

forall s. ST s a

means

forall s. (ST s a)

whereas you'd need it to mean

(forall s. ST s) a

in order for it to unify with (m a).

But then why does "return 42" type successfully as forall s. (ST s a)? It needs that same unification. -Yitz

Brandon S. Allbery KF8NH wrote:

I think the problem is that technically runST is a data constructor (possibly not relevant)

No, at least not in GHC. It is a function.

which takes a function as a parameter (definitely relevant).

It takes the type (forall s. ST s a) as its only parameter. How is that more or less a function than anything else?

In the normal compositional model, (f . g) x = f (g x), you're conceptually invoking f on the result of g x (g is independent of f); here, you're lifting the function g x into the ST s a monad via f (g is dependent on f).

I don't think I am using any special lifting mechanism here. The "return" function does exploit the fact that ST s has a Monad instance, but I only used the "return" function for simplicity. The same thing happens if you construct a function that explicitly returns (forall s. ST s a) and use that instead of "return": Prelude Control.Monad.ST> :set -fglasgow-exts Prelude Control.Monad.ST> let {f :: a -> (forall s. ST s a); f x = return x} Prelude Control.Monad.ST> runST (f 42) 42 Prelude Control.Monad.ST> (runST . f) 42 <interactive>:1:9: Couldn't match expected type `forall s. ST s a' against inferred type `ST s a1' ... Here is another possible clue to what is happening. When I try to define that same function f using monomorphic syntax, it fails: Prelude Control.Monad.ST> let {f :: a -> (forall s. ST s a); f = return} <interactive>:1:39: Inferred type is less polymorphic than expected Quantified type variable `s' escapes Expected type: a -> forall s1. ST s1 a Inferred type: a -> ST s a In the expression: return In the definition of `f': f = return (Of course, the MR is not relevant here, because I am providing an explicit type signature.) _ _ ... ... _ _ -Yitz

On 01/01/07, Yitzchak Gale wrote:

It seems that I can't even use STRefs. Something is really wrong here.

Prelude Control.Monad.ST Data.STRef> runST $ do {r<-newSTRef 2; readSTRef r}

Again, this is due to section 7.4.8 [1] of the GHC user manual, which states that you can't instantiate a type variable with a type involving a forall. You're trying to unify the first parameter of ($) :: a -> b -> a with (forall s. ST s a -> a), which is illegal. Using parentheses works: runST (do r <- newSTRef 2; readSTRef r) However, I'm as much in the dark as you are as to _why_ this is illegal. [1]: http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#uni... -- -David House, dmhouse@gmail.com

Conor and others are right; it's all to do with type inference. There is nothing wrong with the program you are writing, but it's hard to design a type inference algorithm that can figure out what you are doing. The culprit is that you want to instantiate a polymorphic function (here (.) or ($) in your examples) with a higer-rank polymorphic type (the type of runST, in this case). That requires impredicative polymorphism and while GHC now allows that, it only allows it when it's pretty obvious what is going on --- and sadly this case is not obvious enough. The system GHC uses is described in our paper http://research.microsoft.com/~simonpj/papers/boxy Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of | Conor McBride | Sent: 01 January 2007 13:49 | To: haskell-cafe@haskell.org | Subject: Re: [Haskell-cafe] Composing functions with runST | | Hi | | Yitzchak Gale wrote: | > Can anyone explain the following behavior (GHCi 6.6): | | I don't know if I can explain it entirely, or justify it properly, but I | do have some idea what the issue is. Type inference with higher-ran | types is weird. The primary reference is | | Practical type inference for arbitrary-rank types | Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark | Shields. | To appear in the Journal of Functional Programming. | | http://research.microsoft.com/~simonpj/papers/higher-rank/index.htm | | 'The paper is long, but is strongly tutorial in style.' | | Back in the Hindley-Milner days, we knew exactly what polymorphism could | happen where. All the free type variables were existential (hence | specialisable); generalisation over free type variables happened at let. | Unification was untroubled by issues of scope or skolem constants. The | machine could always guess what your idea was because you weren't | allowed to have interesting ideas. | | Now you can ask for polymorphism in funny places by writing non-H-M | types explicitly. As in | | runST :: (forall s. ST s a) -> a | | When you apply runST, you create a non-let source of (compulsory) | polymorphism. You get a new type variable a and a new type constant s, | and the argument is checked against (ST s a). Let's look. | | > Prelude Control.Monad.ST> runST (return 42) | > 42 | | Can (return 42) have type ST s a, for all s and some a? Yes! Instantiate | return's monad to (ST s) and a to the type of 42 (some Num thing? an Int | default?). In made up System F, labelling specialisable unknowns with ? | | runST@?a (/\s. return@(ST s)@?a (42@?a)) such that Num ?a | | Now what's happening here? | | > Prelude Control.Monad.ST> (runST . return) 42 | | We're trying to type an application of (.) | | (.) :: (y -> z) -> (x -> y) -> (x -> z) | | We get two candidates for y, namely what runST wants (forall s. ST s a) | and what return delivers (m b) and these must unify if the functions are | to compose. Oops, they don't. | | The point, I guess, is that application in Haskell source code is no | longer always translated exactly to application in System F. We don't | just get | | (runST@?a) (return@?m@?b) such that (forall s. ST s ?a) = ?m ?b | | we get that extra /\s. inserted for us, thanks to the explicit request | for it in the type of runST. The type of (.) makes no such request. Same | goes for type of ($), so runST behaves differently from (runST $). | | It's a murky world. | | Happy New Year | | Conor | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe

On 1/1/07, Yitzchak Gale wrote:

stToState :: MonadState st m => (STRef s st -> ST s a) -> m a

That would make it very convenient, for example, to use arrays inside a pure state monad.

The type signatures above do ensure (as far as I can see) that the opacity of the ST state thread is not violated. But unfortunately, the protective shield in runST created by the higher-rank polymorphism is too thick.

Probably, stToState :: MonadState st m => (forall s. STRef s st -> ST s a) -> m a E.g. stToState :: MonadState st m => (forall s. STRef s st -> ST s a) -> m a stToState f = do s <- get let (x, s') = runST (do r <- newSTRef s x <- f r s' <- readSTRef r return (x, s')) put s' return x -- Best regerds, Tolik

I wrote:

...

It seems to me that a natural notion of a state transformer in the ST monad is the type: STRef s st -> ST s a

Udo Stenzel wrote:

Are there any useful functions of this type?

Sure. Anything that can be written as a pure state transformer can be written this way, of course. In addition, you can use mutable arrays for speed. Here is a concrete example: Let's say you want to shuffle a large list randomly, within a larger application that lives inside some MTL monad stack. Among other things, your monad m satisfies (RandomGen g, MonadState g m), perhaps after a lift. Well, it turns out that using Data.Sequence or Data.IntMap to shuffle a list becomes prohibitive if you might have more than about 10^5 elements in your list. So in that case you will need to use a mutable array, and you now need ST. Combining ST and MTL can be messy, even in this simple case. You will probably write something with a type like RandomGen g => [a] -> g -> ST s ([a], g) apply runST (tiptoeing carefully around the paradoxes mentioned in this thread), and then build an MTL state thing out of it. Wouldn't it be nice if instead you could just write: shuffle :: (RandomGen g, MonadState g m) => [a] -> m [a] shuffle = stToState . shuffleST

I guess, your intention is that this "transformer" makes no other use of the ST monad than reading or writing a single variable.

Well, it can do whatever it wants inside, but it needs to expose any state that is shared externally. If that state is complex, you can use the same techniques that you would use for a State monad - either build the complexity into the state type using, say, records, or compose several transformers. In this case composition would be: STRef s st1 -> STRef s st2 -> ST s a

It seems, every such function better have a purely functional interface anyway,

Yes, that is the intended use.

even if it makes use of runST internally.

You would not need to, stToState would take care of runST.

...

stToState :: MonadState st m => (STRef s st -> ST s a) -> m a The type signatures above do ensure (as far as I can see) that the opacity of the ST state thread is not violated.

I doubt that. The "transformer" you pass in could have captured references from a different state thread, which is exactly the problem the rank-2 type should prevent.

Hmm, you're right.

I guess, the type signature you want is stToState :: MonadState st m => (forall s . STRef s st -> ST s a) -> m a

Or use some opaque type or monad and do something unsafe inside.

...

Any ideas? A better approach?

Uhm... use MonadState in the first place?

You mean use ST in the first place. Yes, but I want to avoid that.

The converse is comparatively easily accomplished...

Yes. Regards, Yitz

I wrote:

...

Combining ST and MTL can be messy, even in this simple case. You will probably write something with a type like RandomGen g => [a] -> g -> ST s ([a], g)

Udo Stenzel wrote:

But why would you even want to do this? It's ugly and cumbersome.

Yes indeed.

You'd plug a runST in there and get shuffle :: RandomGen g => [a] -> g -> ([a], g)

Yes. In fact, that is what I did in practice. As you say, the overall effect is ugly and cumbersome. And this is with only the simplest of stateful calculations. I shudder to think about what happens when things are more complex. That is why I am thinking that -

...

Wouldn't it be nice if instead you could just write:

shuffle :: (RandomGen g, MonadState g m) => [a] -> m [a] shuffle = stToState . shuffleST

and then just use that directly inside a calculation that is otherwise purely non-ST?

It seems, what you really want is shuffleST :: RandomGen g => [a] -> StateT g ST [a]

Actually, I tried that. It didn't help - it was just one more layer I had to peel away to get at the ST inside. There seems to be no way to avoid the fact that you think about state in two very different ways in these two monads. Every program is written in either one style or the other. Occasionally, you require an isolated use of the opposite style, and I am looking for ways of simplifying the resulting mess. "StateT st ST" and "MonadST" look like ways of combining the two, but in practice I find that they just seem to get in the way. I am starting to be convinced that the only way to write the function I want is by using unsafeRunST. Or type it as stToState :: MonadState st m => (st -> ST s (a, st)) -> m a and then write in the documentation that the user is require to write do r <- newSTRef x ... y <- readSTRef r return (z, y) by hand every time. Yuck. Am I missing something? -Yitz

I wrote:

Am I missing something?

Yes! In reality, I do not need unsafeSTRef for this at all, using a type suggested earlier by Udo: stToState :: MonadState st m => (forall s. STRef s st -> ST s a) -> m a stToState f = do s <- get let (y, s') = runST (stm f s) put s' return y where stm f s = do r <- newSTRef s y <- f r s' <- readSTRef r return (y, s') This works! Thanks, Udo! -Yitz

On 03/01/07, Seth Gordon wrote:

So I can't just tell someone who's just starting to learn Haskell that "f $ g y" is equivalent to "f (g y)"; I have to say "those two are *almost always* equivalent, but if you use $ and the compiler complains about not being able to match the expected and the inferred type and a type signature in the error message has the word 'forall', try rewriting that expression without the $ and see if it compiles". Eeeww.

Why would someone just starting to learn Haskell be using ST? The canonical tutorial structure is to start with the pure stuff and only introduce the (more complicated!) impure stuff (ST, IORefs, etc.) in an 'advanced techniques' or similar section. -- -David House, dmhouse@gmail.com

On 1/3/07, Seth Gordon wrote:

David House wrote:

...

...

So I can't just tell someone who's just starting to learn Haskell that "f $ g y" is equivalent to "f (g y)"; I have to say "those two are *almost always* equivalent, but if you use $ and the compiler complains about not being able to match the expected and the inferred type and a type signature in the error message has the word 'forall', try rewriting that expression without the $ and see if it compiles". Eeeww.

Why would someone just starting to learn Haskell be using ST? The canonical tutorial structure is to start with the pure stuff and only introduce the (more complicated!) impure stuff (ST, IORefs, etc.) in an 'advanced techniques' or similar section.

I (and one other person on this list) ran into this issue when I was trying to use takusen to make Haskell talk to a RDBMS. You obviously need to learn advanced techniques to *implement* such a thing, but you shouldn't need advanced knowledge to *use a library* that happens to use higher-rank polymorphic types in its API.

That other person was me, and I agree entirely. I have a little sample project, using databases and concurrency, which I wanted to rewrite in Haskell, as a learning exercise. I hit exactly this issue when simply trying out some sample code, and my reaction was very much one of irritation, frustration and confusion. One of the nice things about Haskell, coming to it from an imperative POV, is that monads can be thought of a little like first-class composable "statement blocks". When I understood that, I had a real "hey, that's neat!" reaction. One of the nasty things about Haskell (at my level of experience) is that your nice helpful intuitions about monads can break down into real confusion when you hit complex monads, monad transformers and the like - *and you hit them quite early in the APIs of some libraries*! It's not a big deal, but it's a bit offputting for a newcomer. Paul.

On 1/3/07, David House wrote:

On 03/01/07, Seth Gordon wrote:

...

So I can't just tell someone who's just starting to learn Haskell that "f $ g y" is equivalent to "f (g y)"; I have to say "those two are *almost always* equivalent, but if you use $ and the compiler complains about not being able to match the expected and the inferred type and a type signature in the error message has the word 'forall', try rewriting that expression without the $ and see if it compiles". Eeeww.

Why would someone just starting to learn Haskell be using ST? The canonical tutorial structure is to start with the pure stuff and only introduce the (more complicated!) impure stuff (ST, IORefs, etc.) in an 'advanced techniques' or similar section.

(slightly OT) It's true that this is the typical way of learning Haskell, but I for one think it's a bad way of learning Haskell. Very few real world programs get by without the "impure" stuff, so if you give the newbie the impression that it isn't there (by postponing it) there's a chance he'll run into a situation where he needs it before it's been even mentioned (queue newbie going "bah, academic language" and switching to C++). I find that the Haskell introductions I like the most are the ones that accompany papers about STM and such. I.e. ones which have to teach the reader about the basics of Haskell IO, but doesn't have enough space to start with the pretty stuff. Mix that with some actual comutations to show off some pretty stuff and you'll have a newbie who is both excited about the cool looking features of the pure aspects of Haskell, but completely aware of the fact that you can do impure stuff as well. Oh yeah, I agree that the relationship between ($) and (.) is a bit ugly from the user's perspective. It may have very good reasons, but I'd prefer consistency towards the user (i.e. spot when someone is using ($) with higher ranked types and do rewriting) rather than consistency towards the compiler. -- Sebastian Sylvan +46(0)736-818655 UIN: 44640862

It's true that this is the typical way of learning Haskell, but I for one think it's a bad way of learning Haskell. Very few real world programs get by without the "impure" stuff, so if you give the newbie the impression that it isn't there (by postponing it) there's a chance he'll run into a situation where he needs it before it's been even mentioned (queue newbie going "bah, academic language" and switching to C++).

On the contrary, I think it's an excellent way of learning Haskell. I'm writing a lot of useful Haskell code with only one IO action (interact). I don't think I could reasonably construct an introductory problem that couldn't be solved with it, and I haven't yet found an application for which I've needed more. I think it's destructive to teach people "we have a wonderful new paradigm of programming that solves all sorts of problems, but all we're going to use it for is doing what we did with C++ anyway". That's just my 2¢ -- I like Haskell specifically because I don't have to do things in order and I don't have to do things in an imperative style, I would love for more people to be taught about this wonderful thing. Bob

On 1/3/07, Neil Mitchell wrote:

As for beginner issues with rank-2 types, I've been learning Haskell for years now, and have never felt the need for a rank-2 type. If the interface for some feature requires rank-2 types I'd call that an abstraction leak in most cases. It certainly means that you can't properly Hoogle for it, can't compile it with Yhc, can't do full type inference etc.

That may well be true. Something I forgot to mention in my previous posting was that I'm not 100% convinced that the issue I hit with Takusen isn't a problem with the library - I find it very hard to read or understand some parts of the library documentation, basically because the types seem so complex. My intuition says that reading a database is logically similar to reading a file, so types like doQuery :: (Statement stmt sess q, QueryIteratee (DBM mark sess) q i seed b, IQuery q sess b) => stmt -> i -> seed -> DBM mark sess seed look pretty baffling to me - and don't match my intuition that main = do withSession (connect "user" "password" "server") $ do -- simple query, returning reversed list of rows. r <- doQuery (sql "select a, b, c from x") query1Iteratee [] liftIO $ putStrLn $ show r otherActions session is "basically I/O". (Oh, by the way - that "$" on the withSession line is the one that caused the error which started this thread...) Paul.

Hello Yitzchak, Thursday, January 4, 2007, 12:25:41 PM, you wrote:

The other is awkwardness in extending the capabilites of ST. For that, I would propose that the function "unsafeRunST" be added to the library.

this function exists, but named unsafeIOtoST. IO and ST is exactly the same things, the only difference that foreign imports may be marked as IO operations but both ST ones. as a result, ST is restricted to a few standard operations that guarantees to bo be mutually transparent for consumers of runST. when one goes to extend ST functionality, unsafeIOtoST is used. for 3xample, in Hugs it is used to convert peek/poke IO operations into STUArray implementation. except for compile-time type sugar, there is no difference between those two type constructors. unsafeIOtoST is like liftIO: unsafeIOtoST :: IO a -> ST s a -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

Hello Yitzchak, Thursday, January 4, 2007, 4:25:06 PM, you wrote:

...

...

The other is awkwardness in extending the capabilites of ST. For that, I would propose that the function "unsafeRunST" be added to the library.

Bulat Ziganshin wrote:

...

this function exists, but named unsafeIOtoST.

That wasn't what I had in mind, because it forces the thread parameter to take the specific value RealWorld.

this parameter don't have any "physical" meaning at runtime. i still think that it is just what you mean. what other meaning may have unsafeRunST operation? -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

Hi,

On the contrary, I think it's an excellent way of learning Haskell. I'm writing a lot of useful Haskell code with only one IO action (interact). I don't think I could reasonably construct an introductory problem that couldn't be solved with it, and I haven't yet found an application for which I've needed more. I think it's destructive to teach people "we have a wonderful new paradigm of programming that solves all sorts of problems, but all we're going to use it for is doing what we did with C++ anyway".

Yes, but the point is most students have already been poisoned with C++ (or Java). They don't see the point in Haskell becuase they can't see the wood for the trees. The only way to get them interested in Haskell in the first place is to make it look vaguely like C++ (or Java) -- it's like coercing a Donkey with a carrot. Once they are interested - show them there is a lot more to Haskell than imperative-style behaviour, that way they may also see the elegence of purely functional programming.

That's just my 2¢ -- I like Haskell specifically because I don't have to do things in order and I don't have to do things in an imperative style, I would love for more people to be taught about this wonderful thing.

So would I. But in reality it just doesn't seem to work like that. Chris.