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

[MigMit]

Yeah, you're right. Thanks.

On 27 Apr 2014, at 15:03, Roman Cheplyaka <roma at ro-che.info> wrote:

> 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