17

Given the following definitions:

import Control.Monad.ST
import Data.STRef

fourty_two = do
  x <- newSTRef (42::Int)
  readSTRef x

The following compiles under GHC:

main = (print . runST) fourty_two -- (1)

But this does not:

main = (print . runST) $ fourty_two -- (2)

But then as bdonlan points out in a comment, this does compile:

main = ((print . runST) $) fourty_two -- (3)

But, this does not compile

main = (($) (print . runST)) fourty_two -- (4)

Which seems to indicate that (3) only compiles due to special treatment of infix $, however, it still doesn't explain why (1) does compile.

Questions:

1) I've read the following two questions (first, second), and I've been led to believe $ can only be instantiated with monomorphic types. But I would similarly assume . can only be instantiated with monomorphic types, and as a result would similarly fail. Why does the first code succeed but the second code does not? (e.g. is there a special rule GHC has for the first case that it can't apply in the second?)

2) Is there a current GHC extension that compiles the second code? (perhaps ImpredicativePolymorphism did this at some point, but it seems deprecated, has anything replaced it?)

3) Is there any way to define say `my_dollar` using GHC extensions to do what $ does, but is also able to handle polymorphic types, so (print . runST) `my_dollar` fourty_two compiles?

Edit: Proposed Answer:

Also, the following fails to compile:

main = ((.) print runST) fourty_two -- (5)

This is the same as (1), except not using the infix version of ..

As a result, it seems GHC has special rules for both $ and ., but only their infix versions.

9
  • 2
    To make it even more interesting, ( (print . runST) $ ) fourty_two does work
    – bdonlan
    Apr 27, 2012 at 6:33
  • That is interesting and confuses things further!
    – Clinton
    Apr 27, 2012 at 6:37
  • I'm fairly certain that there's a special rule in GHC to support the case runST $ do, but I can't find a cite now.
    – John L
    Apr 27, 2012 at 7:21
  • @John L: Yes, but the second case with the $ does not work, however the first case without $ does. I want to know why the first case does work and the second case doesn't work.
    – Clinton
    Apr 27, 2012 at 7:38
  • 1
    For a real answer, you'll need to find someone intimately familiar with GHC's type-checking algorithm. FYI, ghc-6.12.3 compiles all forms except (3), where it complains that it can't match the forall type with a monotype in the second argument of (.). So the change in the type-checking algorithm between ghc-6 and ghc-7 changed the treatment of forall types as arguments of (.) and ($). From their types, as I understand it, neither should take higher rank types, but that'd be just too inconvenient, so the rules get bent. May 3, 2012 at 11:57

2 Answers 2

6
+50
  1. I'm not sure I understand why the second doesn't work. We can look at the type of print . runST and observe that it is sufficiently polymorphic, so the blame doesn't lie with (.). I suspect that the special rule that GHC has for infix ($) just isn't quite sufficient. SPJ and friends might be open to re-examining it if you propose this fragment as a bug on their tracker.

    As for why the third example works, well, that's just because again the type of ((print . runST) $) is sufficiently polymorphic; in fact, it's equal to the type of print . runST.

  2. Nothing has replaced ImpredicativePolymorphism, because the GHC folks haven't seen any use cases where the extra programmer convenience outweighed the extra potential for compiler bugs. (I don't think they'd see this as compelling, either, though of course I'm not the authority.)
  3. We can define a slightly less polymorphic ($$):

    {-# LANGUAGE RankNTypes #-}
    infixl 0 $$
    ($$) :: ((forall s. f s a) -> b) -> ((forall s. f s a) -> b)
    f $$ x = f x
    

    Then your example typechecks okay with this new operator:

    *Main> (print . runST) $$ fourty_two
    42
    
0

I can't say with too much authority on this subject, but here's what I think may be happening:

Consider what the typechecker has to do in each of these cases. (print . runST) has type Show b => (forall s. ST s t) -> IO (). fourty_two has type ST x Int.

The forall here is an existential type qualifier - here it means that the argument passed in has to be universal on s. That is, you must pass in a polymorphic type that supports any value for s whatsoever. If you don't explicitly state forall, Haskell puts it at the outermost level of the type definition. This means that fourty_two :: forall x. ST x Int and (print . runST) :: forall t. Show t => (forall s. ST s t) -> IO ()

Now, we can match forall x. ST x Int with forall s. ST s t by letting t = Int, x = s. So the direct call case works. What happens if we use $, though?

$ has type ($) :: forall a b. (a -> b) -> a -> b. When we resolve a and b, since the type for $ doesn't have any explicit type scoping like this, the x argument of fourty_two gets lifted out to the outermost scope in the type for ($) - so ($) :: forall x t. (a = forall s. ST s t -> b = IO ()) -> (a = ST x t) -> IO (). At this point, it tries to match a and b, and fails.

If you instead write ((print . runST) $) fourty_two, then the compiler first resolves the type of ((print . runST $). It resolves the type for ($) to be forall t. (a = forall s. ST s t -> b = IO ()) -> a -> b; note that since the second occurance of a is unconstrained, we don't have that pesky type variable leaking out to the outermost scope! And so the match succeeds, the function is partially applied, and the overall type of the expression is forall t. (forall s. ST s t) -> IO (), which is right back where we started, and so it succeeds.

6
  • In the second last paragraph, I don't understand why x gets "lifted". Isn't x an actual type, created by the compiler? From what I understand, it's a hidden type that we can never access, but it's just like say Int. We don't lift Int, why lift x?
    – Clinton
    Apr 27, 2012 at 7:36
  • i.e. isn't x actually X12345, an actual type generated by the compiler (though we'll never have access to it)?
    – Clinton
    Apr 27, 2012 at 7:36
  • @Clinton, x isn't a type, it's a type variable. And I'm not sure why it chooses to lift the implicit quantification on fourty_two to the outer level of the ... $ ... expression type. You can't lift the quantification of Int, though, because that's not a type variable, it's a type.
    – bdonlan
    Apr 28, 2012 at 2:18
  • Ok, but why doesn't s get lifted in (print . runST)?
    – Clinton
    May 3, 2012 at 0:40
  • Presumably because it was explicitly quantified in the first place?
    – bdonlan
    May 3, 2012 at 3:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.