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

[MigMit]

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 <kai at kzhang.org> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe