CODEWITHSUNDEEP
haskellpolymorphism
Clinton
Clinton

Reputation: 23135

Haskell rank two polymorphism compile error

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.

Upvotes: 17

Views: 479

Answers (2)

Daniel Wagner
Daniel Wagner

Reputation: 152867

  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

Upvotes: 6

bdonlan
bdonlan

Reputation: 231213

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.

Upvotes: 0

Related Questions