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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
57 messages Options
123
Reply | Threaded
Open this post in threaded view
|

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

Christopher Allen
$ 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
Reply | Threaded
Open this post in threaded view
|

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

Ryan Scott
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
Reply | Threaded
Open this post in threaded view
|

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

Christopher Allen
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
Reply | Threaded
Open this post in threaded view
|

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

Ben Gamari-2
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 #.
>
Yes, there is a bit of an inconsistency here. As far as I understand
there is still a bit of magic around (->), which allows it to be more
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
Reply | Threaded
Open this post in threaded view
|

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

Ryan Scott
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
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
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
Reply | Threaded
Open this post in threaded view
|

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

Ryan Scott
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
Reply | Threaded
Open this post in threaded view
|

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

Christopher Allen
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".

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
>




--
Chris Allen
Currently working on http://haskellbook.com

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Manuel M T Chakravarty-4
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
Reply | Threaded
Open this post in threaded view
|

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

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



--
Chris Allen
Currently working on http://haskellbook.com

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Edward Z. Yang
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
Reply | Threaded
Open this post in threaded view
|

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

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



--
Chris Allen
Currently working on http://haskellbook.com

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Iavor Diatchki
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:
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
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
> >
>



--
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
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
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:
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
Reply | Threaded
Open this post in threaded view
|

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

Roman Cheplyaka-2
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
Reply | Threaded
Open this post in threaded view
|

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

Joachim Breitner-2
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/.
shouldn’t this already happen, based on -fprint-explicit-kinds? At
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
Reply | Threaded
Open this post in threaded view
|

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

Takenobu Tani
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,

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

shouldn’t this already happen, based on -fprint-explicit-kinds? At
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



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
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:

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,

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

shouldn’t this already happen, based on -fprint-explicit-kinds? At
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


_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

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

Dan Doel

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

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,

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

shouldn’t this already happen, based on -fprint-explicit-kinds? At
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


_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

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

Manuel M T Chakravarty-4
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
123