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

[Roman Cheplyaka]

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>