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

Thu Feb 4 23:20:34 UTC 2016

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