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.

Community
  • 1
  • 1
Clinton
  • 22,361
  • 15
  • 67
  • 163
  • 2
    To make it even more interesting, `( (print . runST) $ ) fourty_two` _does_ work – bdonlan Apr 27 '12 at 06:33
  • That is interesting and confuses things further! – Clinton Apr 27 '12 at 06: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 '12 at 07: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 '12 at 07:38
  • possible duplicate of [runST and function composition](http://stackoverflow.com/questions/9468963/runst-and-function-composition) – Daniel Wagner Apr 27 '12 at 15:03
  • @Daniel Wagner: This question is slightly different. It asks why adding the final `$` makes a difference, not why replacing the first `$` with a `.` makes a difference. Both my examples use the `(a . b)` format, unlike the other question. That question could be answered by GHC's special typing rule, but that doesn't seem to apply here. – Clinton Apr 27 '12 at 15:28
  • Whoops, I didn't even read the question carefully enough to notice you linked to exactly the question I was proposing as a duplicate and explained why it wasn't a duplicate. Sorry! – Daniel Wagner Apr 27 '12 at 18:11
  • 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. – Daniel Fischer May 03 '12 at 11:57
  • I reckon there are some GHC bugs going on here. In this example: http://hpaste.org/68007 numeric defaulting fails to trigger on the literal 5, even though according to the error message the only constraint is `Num`. I can't see any legitimate way that can happen. – Ben Millwood May 04 '12 at 18:54

2 Answers2

6
  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
    
Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
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.

bdonlan
  • 224,562
  • 31
  • 268
  • 324
  • 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 '12 at 07: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 '12 at 07: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 '12 at 02:18
  • Ok, but why doesn't `s` get lifted in (print . runST)? – Clinton May 03 '12 at 00:40
  • Presumably because it was explicitly quantified in the first place? – bdonlan May 03 '12 at 03:04
  • You may be interested in the edited question, in particular, main function (5). It shows there is something special going on with infix `.` – Clinton May 03 '12 at 03:07