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