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

Thu Feb 4 23:38:46 UTC 2016

The sort of pragma you suggest would satisfy me. Pragmas like this don't
bother me and make my job a fair bit easier. Too many, "don't worry about
this; later" is exhausting. Too many, "don't worry about this; we're not
even going to have time to cover it" is demoralizing.

On Thu, Feb 4, 2016 at 5:31 PM, Edward Z. Yang <ezyang at mit.edu> wrote:

> 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
> > >
> >
>

-- 
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/774848dd/attachment.html>