[Haskell-cafe] Why this doesn't work?
Roman Cheplyaka
roma at ro-che.info
Sun Apr 27 11:03:12 UTC 2014
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 <miguelimo38 at yandex.ru> [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 <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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: Digital signature
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140427/98c5e864/attachment.sig>
More information about the Haskell-Cafe
mailing list