Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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.

like image 911
Clinton Avatar asked Apr 27 '12 06:04

Clinton


1 Answers

  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
    
like image 54
Daniel Wagner Avatar answered Oct 16 '22 17:10

Daniel Wagner