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.sc...@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 <c...@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.sc...@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@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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
