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

[Edward Kmett]

Note: (->) is a type. ($) is a term.

There is still magic in the typechecker around allowing fully saturated
applications of (x -> y) allowing x and y to be in either # or *. My
understanding is that (->) isn't really truly levity-polymorphic, but
rather acts differently based on the levity of the argument.

Think of it this way, if you look at what happens on the stack, based on
the kind of the argument and the kind of the result, a value of the type (x
-> y) acts very differently.

Similarly there remain hacks for (x, y) allows x or y to be (both) * or
Constraint through another hack, and () :: Constraint typechecks despite ()
:: * being the default interpretation.

($) and other truly levity polymorphic functions are fortunate in that they
don't need any such magic hacks and don't care.

-Edward

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160205/aac581f5/attachment.html>