Yeah, you're right. Thanks. On 27 Apr 2014, at 15:03, Roman Cheplyaka wrote:

GHC doesn't have a difficulty translating between

a -> forall s. ST s z

and

forall s. a -> ST s z

This is easy to verify:

Prelude> :m +Control.Monad.ST Prelude Control.Monad.ST> :set -XRankNTypes Prelude Control.Monad.ST> let f :: forall a . a -> forall s. ST s a; f = undefined Prelude Control.Monad.ST> :t f f :: a -> ST s a

(and vice versa)

The real problem is that both examples of inference require impredicative instantiation:

...

therefore (a -> b) ~ (forall s. ST s z) -> z therefore a ~ forall s. ST s z, b ~ z

in the first case, and

...

therefore b -> c ~ (forall s. ST s z) -> z therefore b ~ (forall s. ST s z), c ~ z

in the second case. The difference between ($) and (.) is that there's a special case in GHC's type checker for ($) which enables impredicative instantiation, which was added exactly for the common use case of

runST $ ...

Such a rule wasn't added for (.), presumably because people write runST . f much less often, and there weren't as many complaints (perhaps any at all) about (.) not working with runST.

Roman

* MigMit [2014-04-27 14:21:27+0400]

...

runST uses forall. It messes up type inference (and yes, type inference is at play even if top-level function has type signature).

See, if you write "runST $ f x", then GHC deduces this:

($) :: (a -> b) -> a -> b runST :: (forall s. ST s z) -> z therefore (a -> b) ~ (forall s. ST s z) -> z therefore a ~ forall s. ST s z, b ~ z and also f x :: a therefore f x :: forall s. ST s z

Then it goes on checking that f x :: forall s. ST s z actually makes sense, which it does by first stripping away forall and checking that f x :: ST s z is sound.

If you write (runST . f) x, then what GHC sees is

(.) :: (b -> c) -> (a -> b) -> (a -> c) runST :: (forall s. ST s z) -> z therefore b -> c ~ (forall s. ST s z) -> z therefore b ~ (forall s. ST s z), c ~ z and also f :: a -> b therefore f :: a -> forall s. ST s z

Unfortunately, f is of type a -> ST s z, or, if you quantify explicitly, forall s. a -> ST s z. These two types don't match. If you write type arguments explicitly, like you'll do in Agda, you'd have

(s :: Type) -> a -> ST s z

vs

a -> (s :: Type) -> ST s z

So they are different.

I don't think there is an easy way to fix that, apart from using "$".

On 27 Apr 2014, at 12:27, Kai Zhang wrote:

...

Hi Cafe,

I don't understand why this doesn't work:

import qualified Data.Vector.Generic as G import Control.Monad.ST

test :: G.Vector v a => v a -> v a test x = runST . (>>= G.freeze) . G.thaw $ x

But if I replace "." with "$", it can compile.

test x = runST $ (>>= G.freeze) . G.thaw $ x

I originally though f $ g x can always be written as f . g $ x _______________________________________________ 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

Thank you guys! These discussions were very helpful for me to figure out what is going on. On Sun, Apr 27, 2014 at 8:13 AM, Brandon Allbery wrote:

On Sun, Apr 27, 2014 at 7:03 AM, Roman Cheplyaka wrote:

...

runST $ ...

Such a rule wasn't added for (.), presumably because people write runST . f much less often, and there weren't as many complaints (perhaps any at all) about (.) not working with runST.

That, and because they kept trying to fix the real problem (and missing, a lot). A search of the archives will find various Simons grumping about getting it to work right.

-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

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