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

Thu Feb 4 22:56:56 UTC 2016

Out of curiosity, what should the kind of (->) be? Both the argument
and result kind of (->) can be either * or #, but we can't make the
argument kind levity polymorphic due to [1], right? How would you
encode that in a kind signature?

Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/ticket/11473

On Thu, Feb 4, 2016 at 4:15 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I agree with everything that's been said in this thread, including the unstated "that type for ($) is sure ugly".
>
> Currently, saturated (a -> b) is like a language construct, and it has its own typing rule, independent of the type of the type constructor (->). But reading the comment that Ben linked to, I think that comment is out of date. Now that we have levity polymorphism, we can probably to the Right Thing and make the kind of (->) more flexible.
>
> Richard
>
> On Feb 4, 2016, at 3:27 PM, Ryan Scott <ryan.gl.scott at gmail.com> wrote:
>
>>> 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
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>