> 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 <e...@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.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 > > > > -- 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
