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

[Ryan Scott]

> 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 <cma at bitemyapp.com> 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 <ryan.gl.scott at gmail.com> 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
>
> --
> Chris Allen
> Currently working on http://haskellbook.com