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

Thu Feb 4 23:31:35 UTC 2016

I'm not really sure how you would change the type of 'id' based on
a language pragma.

How do people feel about a cosmetic fix, where we introduce a new
pragma, {-# LANGUAGE ShowLevity #-} which controls the display of levity
arguments/TYPE.  It's off by default but gets turned on by some
extensions like MagicHash (i.e. we only show levity if you have
enabled extensions where the distinction matters).

Edward

Excerpts from Christopher Allen's message of 2016-02-04 15:20:34 -0800:
> This seems worse than FTP IMO. It's considerably noisier, considerably
> rarer a concern for Haskell programmers, and is wayyyy beyond the scope of
> most learning resources.
> 
> Is there a reason this isn't behind a pragma?
> 
> On Thu, Feb 4, 2016 at 5:02 PM, Manuel M T Chakravarty <chak at justtesting.org
> > wrote:
> 
> > To be honest, I think, it is quite problematic if an obscure and untested
> > language extension (sorry, but that’s what it is right now) bleeds through
> > into supposedly simple standard functionality. The beauty of most of GHC’s
> > language extensions is that you can ignore them until you need them.
> >
> > Has this ever been discussed more widely? I expect that every single
> > person teaching Haskell is going to be unhappy about it.
> >
> > Manuel
> >
> >
> > > Richard Eisenberg <eir at cis.upenn.edu>:
> > >
> > > 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
> > >>
> > >
> > > _______________________________________________
> > > ghc-devs mailing list
> > > ghc-devs at haskell.org
> > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >
> 