Re: [Haskell-cafe] Why this doesn't work?

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