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

[Christopher Allen]

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