Re: New type of ($) operator in GHC 8.0 is problematic

My understanding was that the implicitly polymorphic levity, did (->) not change because it's a type constructor?

The kind of (->) as GHCi reports it is technically correct. As a kind constructor, (->) has precisely the kind * -> * -> *. What's special about (->) is that when you have a saturated application of it, it takes on a levity-polymorphic kind. For example, this: :k (->) Int# Int# would yield a kind error, but :k Int# -> Int# is okay. Now, if you want an explanation as to WHY that's the case, I don't think I could give one, as I simply got this information from [1] (see the fourth bullet point, for OpenKind). Perhaps SPJ or Richard Eisenberg could give a little insight here.

Also does this encapsulate the implicit impredicativity of ($) for making runST $ work? I don't presently see how it would.

You're right, the impredicativity hack is a completely different thing. So while you won't be able to define your own ($) and be able to (runST $ do ...), you can at least define your own ($) and have it work with unlifted return types. :) Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds On Thu, Feb 4, 2016 at 2:53 PM, Christopher Allen wrote:

My understanding was that the implicitly polymorphic levity, did (->) not change because it's a type constructor?

Prelude> :info (->) data (->) a b -- Defined in ‘GHC.Prim’ Prelude> :k (->) (->) :: * -> * -> *

Basically I'm asking why ($) changed and (->) did not when (->) had similar properties WRT * and #.

Also does this encapsulate the implicit impredicativity of ($) for making runST $ work? I don't presently see how it would.

Worry not about the book, we already hand-wave FTP effectively. One more type shouldn't change much.

Thank you very much for answering, this has been very helpful already :)

--- Chris

On Thu, Feb 4, 2016 at 12:52 PM, Ryan Scott wrote:

...

Hi Chris,

The change to ($)'s type is indeed intentional. The short answer is that ($)'s type prior to GHC 8.0 was lying a little bit. If you defined something like this:

unwrapInt :: Int -> Int# unwrapInt (I# i) = i

You could write an expression like (unwrapInt $ 42), and it would typecheck. But that technically shouldn't be happening, since ($) :: (a -> b) -> a -> b, and we all know that polymorphic types have to live in kind *. But if you look at unwrapInt :: Int -> Int#, the type Int# certainly doesn't live in *. So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. OpenKind is an awful hack that allows both lifted (kind *) and unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42) typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg extended the type system with levity polymorphism [1] to indicate in the type signature where these kind of scenarios are happening.

So in the "new" type signature for ($):

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b

The type b can either live in kind * (which is now a synonym for TYPE 'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is indicated by the fact that TYPE w is polymorphic in its levity type w.

Truth be told, there aren't that many Haskell functions that actually levity polymorphic, since normally having an argument type that could live in either * or # would wreak havoc with the RTS (otherwise, how would it know if it's dealing with a pointer or a value on the stack?). But as it turns out, it's perfectly okay to have a levity polymorphic type in a non-argument position [2]. Indeed, in the few levity polymorphic functions that I can think of:

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b error :: forall (v :: Levity) (a :: TYPE v). HasCallStack => [Char] -> a undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a

The levity polymorphic type never appears directly to the left of an arrow.

The downside of all this is, of course, that the type signature of ($) might look a lot scarier to beginners. I'm not sure how you'd want to deal with this, but for 99% of most use cases, it's okay to lie and state that ($) :: (a -> b) -> a -> b. You might have to include a disclaimer that if they type :t ($) into GHCi, they should be prepared for some extra information!

Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds [2] https://ghc.haskell.org/trac/ghc/ticket/11473 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

-- Chris Allen Currently working on http://haskellbook.com