[Haskell-cafe] Why this doesn't work?
MigMit
miguelimo38 at yandex.ru
Sun Apr 27 10:21:27 UTC 2014
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
More information about the Haskell-Cafe
mailing list