$ ghci :lGHCi, version 8.0.0.20160122: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/callen/.ghci Prelude> :t ($) ($) :: forall (w :: GHC.Types.Levity) a (b :: TYPE w). (a -> b) -> a -> b As someone that's working on a book for beginners/intermediates and that mentions ($) early'ish, this is pretty disconcerting. Particularly as we're not going to explain Levity or TYPE. Is this intentional? My only ~/.ghci flag is fno-warn-type-defaults. Apologies if this is a mix-up on my part. --- Chris _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> wrote: Hi Chris, Chris Allen Currently working on http://haskellbook.com _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Christopher Allen <[hidden email]> writes:
> 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 #. > polymorphic than it appears. There's a bit of evidence of this magic here [1]. Cheers, - Ben [1] https://github.com/ghc/ghc/blob/84b0ebedd09fcfbda8efd7576dce9f52a2b6e6ca/compiler/prelude/TysPrim.hs#L262 _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs signature.asc (482 bytes) Download Attachment |
In reply to this post by Christopher Allen
> 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 <[hidden email]> 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 <[hidden email]> 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 >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > > > -- > Chris Allen > Currently working on http://haskellbook.com ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 >>> [hidden email] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >> >> >> >> -- >> Chris Allen >> Currently working on http://haskellbook.com > _______________________________________________ > ghc-devs mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Out of curiosity, what should the kind of (->) be? Both the argument
and result kind of (->) can be either * or #, but we can't make the argument kind levity polymorphic due to [1], right? How would you encode that in a kind signature? Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/ticket/11473 On Thu, Feb 4, 2016 at 4:15 PM, Richard Eisenberg <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 >>>> [hidden email] >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>> >>> >>> >>> >>> -- >>> Chris Allen >>> Currently working on http://haskellbook.com >> _______________________________________________ >> ghc-devs mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Richard Eisenberg-2
> 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 <[hidden email]> wrote: I agree with everything that's been said in this thread, including the unstated "that type for ($) is sure ugly". Chris Allen Currently working on http://haskellbook.com _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Richard Eisenberg-2
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 <[hidden email]>: > > 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 >>>> [hidden email] >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>> >>> >>> >>> >>> -- >>> Chris Allen >>> Currently working on http://haskellbook.com >> _______________________________________________ >> ghc-devs mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > > _______________________________________________ > ghc-devs mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> 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. Chris Allen Currently working on http://haskellbook.com _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
I'm not really sure how you would change the type of 'id' based on
a language pragma. How do people feel about a cosmetic fix, where we introduce a new pragma, {-# LANGUAGE ShowLevity #-} which controls the display of levity arguments/TYPE. It's off by default but gets turned on by some extensions like MagicHash (i.e. we only show levity if you have enabled extensions where the distinction matters). Edward Excerpts from Christopher Allen's message of 2016-02-04 15:20:34 -0800: > 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 <[hidden email] > > 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 <[hidden email]>: > > > > > > 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 <[hidden email]> 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 <[hidden email]> > > 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 <[hidden email]> > > 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 > > >>>> [hidden email] > > >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > >>> > > >>> > > >>> > > >>> > > >>> -- > > >>> Chris Allen > > >>> Currently working on http://haskellbook.com > > >> _______________________________________________ > > >> ghc-devs mailing list > > >> [hidden email] > > >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > >> > > > > > > _______________________________________________ > > > ghc-devs mailing list > > > [hidden email] > > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > > _______________________________________________ > > ghc-devs mailing list > > [hidden email] > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
The sort of pragma you suggest would satisfy me. Pragmas like this don't bother me and make my job a fair bit easier. Too many, "don't worry about this; later" is exhausting. Too many, "don't worry about this; we're not even going to have time to cover it" is demoralizing. On Thu, Feb 4, 2016 at 5:31 PM, Edward Z. Yang <[hidden email]> wrote: I'm not really sure how you would change the type of 'id' based on Chris Allen Currently working on http://haskellbook.com _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Hello, how about we simply use two operators: 1. ($) which only works for standard types (i.e., not #), which we can use 99% of the time, and 2. some other operator which has the levity polymorphic type and would be used in the advanced cases when you are working with unboxed values, etc. Personally, I use unboxed values rarely enough, that I'd even be OK simply using parens or naming the sub-expression instead of using $ -Iavor On Thu, Feb 4, 2016 at 5:38 PM, Christopher Allen <[hidden email]> wrote:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Christopher Allen
Note: (->) is a type. ($) is a term. There is still magic in the typechecker around allowing fully saturated applications of (x -> y) allowing x and y to be in either # or *. My understanding is that (->) isn't really truly levity-polymorphic, but rather acts differently based on the levity of the argument. Think of it this way, if you look at what happens on the stack, based on the kind of the argument and the kind of the result, a value of the type (x -> y) acts very differently. Similarly there remain hacks for (x, y) allows x or y to be (both) * or Constraint through another hack, and () :: Constraint typechecks despite () :: * being the default interpretation. ($) and other truly levity polymorphic functions are fortunate in that they don't need any such magic hacks and don't care. -Edward On Thu, Feb 4, 2016 at 2:53 PM, Christopher Allen <[hidden email]> wrote:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Edward Z. Yang
On 02/05/2016 01:31 AM, Edward Z. Yang wrote:
> I'm not really sure how you would change the type of 'id' based on > a language pragma. > > How do people feel about a cosmetic fix, where we introduce a new > pragma, {-# LANGUAGE ShowLevity #-} which controls the display of levity > arguments/TYPE. It's off by default but gets turned on by some > extensions like MagicHash (i.e. we only show levity if you have > enabled extensions where the distinction matters). Yes, I am surprised this isn't the way it's been done. The levity arguments should totally be hidden unless requested explicitly. I'd only expect this to be a ghc flag (-fshow-levity), not a language pragma, since it should only affect the way types are /shown/. Roman _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs signature.asc (836 bytes) Download Attachment |
Hi,
Am Freitag, den 05.02.2016, 09:22 +0200 schrieb Roman Cheplyaka: > On 02/05/2016 01:31 AM, Edward Z. Yang wrote: > > I'm not really sure how you would change the type of 'id' based on > > a language pragma. > > > > How do people feel about a cosmetic fix, where we introduce a new > > pragma, {-# LANGUAGE ShowLevity #-} which controls the display of > > levity > > arguments/TYPE. It's off by default but gets turned on by some > > extensions like MagicHash (i.e. we only show levity if you have > > enabled extensions where the distinction matters). > > Yes, I am surprised this isn't the way it's been done. The levity > arguments should totally be hidden unless requested explicitly. > > I'd only expect this to be a ghc flag (-fshow-levity), not a language > pragma, since it should only affect the way types are /shown/. least I would have expected this. So we probably either want to make sure that -fno-print-explicit-kinds also prevents forall’ed kind variables, or add a new flag of that (heh) kind. Greetings, Joachim -- Joachim “nomeata” Breitner [hidden email] • http://www.joachim-breitner.de/ Jabber: [hidden email] • GPG-Key: 0xF0FBF51F Debian Developer: [hidden email] _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs signature.asc (836 bytes) Download Attachment |
Hi, I'll worry about the learning curve of beginners. Maybe, beginners will try following session in their 1st week. ghci> :t foldr ghci> :t ($) They'll get following result. Before ghc7.8: Prelude> :t foldr foldr :: (a -> b -> b) -> b -> [a] -> b Prelude> :t ($) ($) :: (a -> b) -> a -> b Beginners should only understand about following: * type variable (polymorphism) After ghc8.0: Prelude> :t foldr foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b Prelude> :t ($) ($) :: forall (w :: GHC.Types.Levity) a (b :: TYPE w). (a -> b) -> a -> b Beginners should understand about following things, more: * higher order polymorphism (t m) * type class (class t =>) * universal quantification (forall) * kind (type::kind) * levity (lifted/unlifted) I think it's harder in their 1st week. I tried to draw informal illustrations about Foldable, but beginners may need ghci-beginner’s mode or something? Sorry I don't still have good idea. Of course I like Haskell's abstraction :) Regards, Takenobu 2016-02-05 18:19 GMT+09:00 Joachim Breitner <[hidden email]>: Hi, _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
As the instigator of these most recent changes: - Yes, absolutely, ($)'s type is quite ugly. In other areas, I've tried to hide the newfound complexity in the type system behind flags, but I missed this one. I consider the current output to be a bug. - It's conceivable to have a flag -fdefault-levity, on by default, which looks for levity polymorphism while printing and instantiates all levity variables to Lifted before printing. That would fix the type of ($). Of course, users could specify -fno-default-levity. Would this make you happy? - There's a real drawback to flags like -fdefault-levity (and, relatedly, -fprint-explicit-kinds, -fprint-explicit-foralls, -fprint-explicit-coercions, -fprint-equality-relations; the last two are new in 8.0): they hide things from unsuspecting users. We already get a steady trickle of bug reports stemming from confusion around hidden kinds. Users diligently try to make a minimal test case and then someone has to point out that the user is wrong. It's a waste of time and, I'm sure, is frustrating for users. I'm worried about this problem getting worse. - It's interesting that the solution to the two problems Takenobu pulls out below (but others have hinted at in this thread) is by having an alternate Prelude for beginners. I believe that having an alternate beginners' Prelude is becoming essential. I know I'm not the first one to suggest this, but a great many issues that teachers of Haskell have raised with me and posts on this and other lists would be solved by an alternate Prelude for beginners. - Separate from a full alternate Prelude, and as Iavor suggested, we could just have two ($) operators: a simple one with no baked-in magic or levity polymorphism, and then a levity-polymorphic, sneakily impredicative one. This would be dead easy. - Edward is right in that (->) isn't really levity-polymorphic. Well, it is, but it's ad hoc polymorphism not parametric polymorphism. Perhaps in the future we'll make this more robust by actually using type-classes to control it, as we probably should. - The case with (->) is different than that with (). (() :: Constraint) and (() :: *) are wholly unrelated types. () is not constraintyness-polymorphic. It's just that we have two wholly unrelated types that happen to share a spelling. So there are hacks in the compiler to disambiguate. Sometimes these hacks do the wrong thing. If we had type-directed name resolution (which I'm not proposing to have!), this would get resolved nicely. - The reason that the foralls get printed in ($)'s type is that kind variables appear in the type variables' kinds. GHC thinks that printing the foralls are useful in this case and does so without a flag. This is not directly related to the levity piece. If you say `:t Proxy`, you'll get similar behavior. Bottom line: We *need* an alternate Prelude. But that won't happen for 8.0. So in the meantime, I propose -fdefault-levity, awaiting your approval. Richard On Feb 5, 2016, at 8:16 AM, Takenobu Tani <[hidden email]> wrote:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
I have a side question and some possible alternate views on a couple things. The first is: is the fancy type of ($) actually used? It has additional special type checking behavior that isn't captured in that type (impredicative instantiation), but probably in a separate code path. Does that only happen when it's saturated or something, and this is for partial applications? Second, it seems like () being overloaded is exactly like type classes, and (->) is less clearly in that camp (it seems more like a gadt). Just, we don't have classes at the level necessary to handle (). -- Dan On Feb 5, 2016 8:49 AM, "Richard Eisenberg" <[hidden email]> wrote:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by Roman Cheplyaka-2
That makes a lot of sense to me.
Manuel > Roman Cheplyaka <[hidden email]>: > > On 02/05/2016 01:31 AM, Edward Z. Yang wrote: >> I'm not really sure how you would change the type of 'id' based on >> a language pragma. >> >> How do people feel about a cosmetic fix, where we introduce a new >> pragma, {-# LANGUAGE ShowLevity #-} which controls the display of levity >> arguments/TYPE. It's off by default but gets turned on by some >> extensions like MagicHash (i.e. we only show levity if you have >> enabled extensions where the distinction matters). > > Yes, I am surprised this isn't the way it's been done. The levity > arguments should totally be hidden unless requested explicitly. > > I'd only expect this to be a ghc flag (-fshow-levity), not a language > pragma, since it should only affect the way types are /shown/. > > Roman > > _______________________________________________ > ghc-devs mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Free forum by Nabble | Edit this page |