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

Thu Feb 4 22:57:33 UTC 2016

> make the kind of (->) more flexible.

Can that wait until 8.2 so we don't have to edit the book as much in
preparation for 8.0? :P

On Thu, Feb 4, 2016 at 3:15 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:

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

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