57

Why does this typecheck:

runST $ return $ True

While the following does not:

runST . return $ True

GHCI complains:

Couldn't match expected type `forall s. ST s c0'
            with actual type `m0 a0'
Expected type: a0 -> forall s. ST s c0
  Actual type: a0 -> m0 a0
In the second argument of `(.)', namely `return'
In the expression: runST . return
Grzegorz Chrupała
  • 3,053
  • 17
  • 24
  • 7
    If `($)` could be given a depedently typed signature as `($) : forall (a : *) (b : a -> *) . ((x : a) -> b x) -> (x : a) -> b x` it would work without GHC tricks, and similarly for `(.)`. – danr Feb 27 '12 at 20:16

3 Answers3

53

The short answer is that type inference doesn't always work with higher-rank types. In this case, it is unable to infer the type of (.), but it type checks if we add an explicit type annotation:

> :m + Control.Monad.ST
> :set -XRankNTypes
> :t (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True
(((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True :: Bool

The same problem also happens with your first example, if we replace ($) with our own version:

> let app f x = f x
> :t runST `app` (return `app` True)
<interactive>:1:14:
    Couldn't match expected type `forall s. ST s t0'
                with actual type `m0 t10'
    Expected type: t10 -> forall s. ST s t0
      Actual type: t10 -> m0 t10
    In the first argument of `app', namely `return'
    In the second argument of `app', namely `(return `app` True)'

Again, this can be solved by adding type annotations:

> :t (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True)
(app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) :: Bool

What is happening here is that there is a special typing rule in GHC 7 which only applies to the standard ($) operator. Simon Peyton-Jones explains this behavior in a reply on the GHC users mailing list:

This is a motivating example for type inference that can deal with impredicative types. Consider the type of ($):

($) :: forall p q. (p -> q) -> p -> q

In the example we need to instantiate p with (forall s. ST s a), and that's what impredicative polymorphism means: instantiating a type variable with a polymorphic type.

Sadly, I know of no system of reasonable complexity that can typecheck [this] unaided. There are plenty of complicated systems, and I have been a co-author on papers on at least two, but they are all Too Jolly Complicated to live in GHC. We did have an implementation of boxy types, but I took it out when implementing the new typechecker. Nobody understood it.

However, people so often write

runST $ do ...

that in GHC 7 I implemented a special typing rule, just for infix uses of ($). Just think of (f $ x) as a new syntactic form, with the obvious typing rule, and away you go.

Your second example fails because there is no such rule for (.).

hammar
  • 138,522
  • 17
  • 304
  • 385
36

The runST $ do { ... } pattern is so common, and the fact that it normally wouldn't type-check is so annoying, that GHC included some ST-specific type-checking hacks to make it work. Those hacks are probably firing here for the ($) version, but not the (.) version.

Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
  • Interesting point. It is probably enough to simply drop the ($) as soon as it is seen that it is applied to 2 arguments. Should be easily verifiable by replacing it with a custom function that does the same as ($), and look if the type checker would complain then. – Ingo Feb 27 '12 at 18:37
  • 1
    @Ingo: Yep, ```let app f x = f x in runST `app` (return `app` True)``` fails to type check. Interesting. – hammar Feb 27 '12 at 18:53
  • 1
    @Hammar: This means, GHC apparently drops the $ despite this is not quite correct with higher rank types. – Ingo Feb 27 '12 at 19:08
  • 1
    This is the correct answer. The first snippet wouldn't normally typecheck, however, GHC has a special rule for `runST $ whatever`, but not for `runST . foo`. – Daniel Fischer Feb 27 '12 at 21:23
  • 3
    And not for `($) runST (return True)` which doesn't typecheck either – Ed'ka Feb 27 '12 at 23:00
3

The messages are a bit confusing the point (or so I feel). Let me rewrite your code:

runST (return True)   -- return True is ST s Bool
(runST . return) True  -- cannot work

Another way to put this is that the monomorphic m0 a0 (the result of return, if it would get an a0) cannot be unified with (forall s.ST s a).

Ingo
  • 36,037
  • 5
  • 53
  • 100
  • This does typecheck: `unsafePerformIO . return $ True` – Grzegorz Chrupała Feb 27 '12 at 18:07
  • 4
    @Ingo: You're parsing the two examples wrong. `runST $ return $ True` is `($) runST (($) return True)`, and `runST . return $ True` is `($) ((.) runST return) True`. They would do the same thing in the absence of rank-2 types. – ehird Feb 27 '12 at 18:08
  • 1
    @ehird - You're right, I forgot the dot. (Hey, that rhymes ...) – Ingo Feb 27 '12 at 18:27