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

...

Hi Chris,

The change to ($)'s type is indeed intentional. The short answer is that ($)'s type prior to GHC 8.0 was lying a little bit. If you defined something like this:

unwrapInt :: Int -> Int# unwrapInt (I# i) = i

You could write an expression like (unwrapInt $ 42), and it would typecheck. But that technically shouldn't be happening, since ($) :: (a -> b) -> a -> b, and we all know that polymorphic types have to live in kind *. But if you look at unwrapInt :: Int -> Int#, the type Int# certainly doesn't live in *. So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. OpenKind is an awful hack that allows both lifted (kind *) and unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42) typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg extended the type system with levity polymorphism [1] to indicate in the type signature where these kind of scenarios are happening.

So in the "new" type signature for ($):

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b

The type b can either live in kind * (which is now a synonym for TYPE 'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is indicated by the fact that TYPE w is polymorphic in its levity type w.

Truth be told, there aren't that many Haskell functions that actually levity polymorphic, since normally having an argument type that could live in either * or # would wreak havoc with the RTS (otherwise, how would it know if it's dealing with a pointer or a value on the stack?). But as it turns out, it's perfectly okay to have a levity polymorphic type in a non-argument position [2]. Indeed, in the few levity polymorphic functions that I can think of:

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b error :: forall (v :: Levity) (a :: TYPE v). HasCallStack => [Char] -> a undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a

The levity polymorphic type never appears directly to the left of an arrow.

The downside of all this is, of course, that the type signature of ($) might look a lot scarier to beginners. I'm not sure how you'd want to deal with this, but for 99% of most use cases, it's okay to lie and state that ($) :: (a -> b) -> a -> b. You might have to include a disclaimer that if they type :t ($) into GHCi, they should be prepared for some extra information!

Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds [2] https://ghc.haskell.org/trac/ghc/ticket/11473 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

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

...

Hi Chris,

The change to ($)'s type is indeed intentional. The short answer is that ($)'s type prior to GHC 8.0 was lying a little bit. If you defined something like this:

unwrapInt :: Int -> Int# unwrapInt (I# i) = i

You could write an expression like (unwrapInt $ 42), and it would typecheck. But that technically shouldn't be happening, since ($) :: (a -> b) -> a -> b, and we all know that polymorphic types have to live in kind *. But if you look at unwrapInt :: Int -> Int#, the type Int# certainly doesn't live in *. So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. OpenKind is an awful hack that allows both lifted (kind *) and unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42) typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg extended the type system with levity polymorphism [1] to indicate in the type signature where these kind of scenarios are happening.

So in the "new" type signature for ($):

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b

The type b can either live in kind * (which is now a synonym for TYPE 'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is indicated by the fact that TYPE w is polymorphic in its levity type w.

Truth be told, there aren't that many Haskell functions that actually levity polymorphic, since normally having an argument type that could live in either * or # would wreak havoc with the RTS (otherwise, how would it know if it's dealing with a pointer or a value on the stack?). But as it turns out, it's perfectly okay to have a levity polymorphic type in a non-argument position [2]. Indeed, in the few levity polymorphic functions that I can think of:

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b error :: forall (v :: Levity) (a :: TYPE v). HasCallStack => [Char] -> a undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a

The levity polymorphic type never appears directly to the left of an arrow.

The downside of all this is, of course, that the type signature of ($) might look a lot scarier to beginners. I'm not sure how you'd want to deal with this, but for 99% of most use cases, it's okay to lie and state that ($) :: (a -> b) -> a -> b. You might have to include a disclaimer that if they type :t ($) into GHCi, they should be prepared for some extra information!

Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds [2] https://ghc.haskell.org/trac/ghc/ticket/11473 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 :

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

...

Hi Chris,

The change to ($)'s type is indeed intentional. The short answer is that ($)'s type prior to GHC 8.0 was lying a little bit. If you defined something like this:

unwrapInt :: Int -> Int# unwrapInt (I# i) = i

You could write an expression like (unwrapInt $ 42), and it would typecheck. But that technically shouldn't be happening, since ($) :: (a -> b) -> a -> b, and we all know that polymorphic types have to live in kind *. But if you look at unwrapInt :: Int -> Int#, the type Int# certainly doesn't live in *. So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. OpenKind is an awful hack that allows both lifted (kind *) and unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42) typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg extended the type system with levity polymorphism [1] to indicate in the type signature where these kind of scenarios are happening.

So in the "new" type signature for ($):

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b

The type b can either live in kind * (which is now a synonym for TYPE 'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is indicated by the fact that TYPE w is polymorphic in its levity type w.

Truth be told, there aren't that many Haskell functions that actually levity polymorphic, since normally having an argument type that could live in either * or # would wreak havoc with the RTS (otherwise, how would it know if it's dealing with a pointer or a value on the stack?). But as it turns out, it's perfectly okay to have a levity polymorphic type in a non-argument position [2]. Indeed, in the few levity polymorphic functions that I can think of:

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b error :: forall (v :: Levity) (a :: TYPE v). HasCallStack => [Char] -> a undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a

The levity polymorphic type never appears directly to the left of an arrow.

The downside of all this is, of course, that the type signature of ($) might look a lot scarier to beginners. I'm not sure how you'd want to deal with this, but for 99% of most use cases, it's okay to lie and state that ($) :: (a -> b) -> a -> b. You might have to include a disclaimer that if they type :t ($) into GHCi, they should be prepared for some extra information!

Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds [2] https://ghc.haskell.org/trac/ghc/ticket/11473 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

...

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 :

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

...

Hi Chris,

The change to ($)'s type is indeed intentional. The short answer is that ($)'s type prior to GHC 8.0 was lying a little bit. If you defined something like this:

unwrapInt :: Int -> Int# unwrapInt (I# i) = i

You could write an expression like (unwrapInt $ 42), and it would typecheck. But that technically shouldn't be happening, since ($) :: (a -> b) -> a -> b, and we all know that polymorphic types have to live in kind *. But if you look at unwrapInt :: Int -> Int#, the type Int# certainly doesn't live in *. So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. OpenKind is an awful hack that allows both lifted (kind *) and unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42) typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg extended the type system with levity polymorphism [1] to indicate in the type signature where these kind of scenarios are happening.

So in the "new" type signature for ($):

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b

The type b can either live in kind * (which is now a synonym for TYPE 'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is indicated by the fact that TYPE w is polymorphic in its levity type w.

Truth be told, there aren't that many Haskell functions that actually levity polymorphic, since normally having an argument type that could live in either * or # would wreak havoc with the RTS (otherwise, how would it know if it's dealing with a pointer or a value on the stack?). But as it turns out, it's perfectly okay to have a levity polymorphic type in a non-argument position [2]. Indeed, in the few levity polymorphic functions that I can think of:

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a

-> b

...

error :: forall (v :: Levity) (a :: TYPE v). HasCallStack => [Char] -> a undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a

The levity polymorphic type never appears directly to the left of an arrow.

The downside of all this is, of course, that the type signature of ($) might look a lot scarier to beginners. I'm not sure how you'd want to deal with this, but for 99% of most use cases, it's okay to lie and state that ($) :: (a -> b) -> a -> b. You might have to include a disclaimer that if they type :t ($) into GHCi, they should be prepared for some extra information!

Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds [2] https://ghc.haskell.org/trac/ghc/ticket/11473 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

...

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 < chak@justtesting.org

...

wrote:

...

To be honest, I think, it is quite problematic if an obscure and untested language extension (sorry, but that’s what it is right now) bleeds

...

...

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 :

I agree with everything that's been said in this thread, including

...

...

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

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 < cma@bitemyapp.com> wrote: > My understanding was that the implicitly polymorphic levity, did (->) not > change because it's a type constructor? > > Prelude> :info (->) > data (->) a b -- Defined in ‘GHC.Prim’ > Prelude> :k (->) > (->) :: * -> * -> * > > Basically I'm asking why ($) changed and (->) did not when (->) had similar > properties WRT * and #. > > Also does this encapsulate the implicit impredicativity of ($) for making > runST $ work? I don't presently see how it would. > > Worry not about the book, we already hand-wave FTP effectively. One more > type shouldn't change much. > > Thank you very much for answering, this has been very helpful already :) > > --- Chris > > > On Thu, Feb 4, 2016 at 12:52 PM, Ryan Scott < ryan.gl.scott@gmail.com> wrote: >> >> Hi Chris, >> >> The change to ($)'s type is indeed intentional. The short answer is >> that ($)'s type prior to GHC 8.0 was lying a little bit. If you >> defined something like this: >> >> unwrapInt :: Int -> Int# >> unwrapInt (I# i) = i >> >> You could write an expression like (unwrapInt $ 42), and it would >> typecheck. But that technically shouldn't be happening, since ($) :: >> (a -> b) -> a -> b, and we all know that polymorphic types have to >> live in kind *. But if you look at unwrapInt :: Int -> Int#, the type >> Int# certainly doesn't live in *. So why is this happening? >> >> The long answer is that prior to GHC 8.0, in the type signature ($) :: >> (a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind. >> OpenKind is an awful hack that allows both lifted (kind *) and >> unlifted (kind #) types to inhabit it, which is why (unwrapInt $

...

...

...

...

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

Excerpts from Christopher Allen's message of 2016-02-04 15:20:34 -0800: through the 42) prepared

...

...

...

...

>> for some extra information! >> >> Ryan S. >> ----- >> [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds >> [2] https://ghc.haskell.org/trac/ghc/ticket/11473 >> _______________________________________________ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > > > -- > Chris Allen > Currently working on http://haskellbook.com _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0xF0FBF51F Debian Developer: nomeata@debian.org

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 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 : 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 mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0xF0FBF51F Debian Developer: nomeata@debian.org

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On 05.02.2016 14:49, Richard Eisenberg wrote:

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

Could you make (->) work for values of types of user defined kinds? -- Wojtek

On Fri, Feb 5, 2016 at 2:16 PM, Takenobu Tani 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

If the output was the following it would be more understandable (and more encouraging!) """ Prelude> :t foldr foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b For example: foldr :: (a -> b -> b) -> b -> [a] -> b foldr :: (a -> b -> b) -> b -> Maybe a -> b foldr :: (a -> b -> b) -> b -> Identity a -> b foldr :: (a -> b -> b) -> b -> (c, a) -> b and more """ It is easy to see a pattern here. The order of the instances used could be the load order, so the ones from Prelude would come first.

Prelude> :t ($) ($) :: forall (w :: GHC.Types.Levity) a (b :: TYPE w). (a -> b) -> a -> b

I'm not sure how this would work here, but when Levity is *, this should collapse into the old syntax, so: """ Prelude> :t ($) ($) :: <"unreadable blurb"> For example: ($) :: (a -> b) -> a -> b ($) :: forall a (b :: #). (a -> b) -> a -> b """ At least one of those lines should be understandable. Alexander

That makes a lot of sense to me. Manuel

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

Roman

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

This approach wouldn't quite work. - It seems to kick in only when instantiating a Levity variable. That would not happen when using :info. - It is possible to have unlifted types about even without -XMagicHash. -XMagicHash is simply a lexer extension, nothing more. By convention, we use the # suffix with unlifted things, but there's no requirement here. Having -XMagicHash thus imply a flag about the type system is bizarre. Furthermore, I'm not sure what the practical, user-visible improvement would be over the approach you include and the -fshow-runtime-rep idea. Richard On Feb 13, 2016, at 11:40 AM, Yuras Shumovich wrote:

Thank you for the summary! The thread is too big to find anything in it.

I'd like to present a bit different approach, kind of a compromise, without lie and code breakage: introduce a language pragma for levity polymorphism and default levity polymorphic signatures to "*" when the pragma is not enabled.

For example, ($) could be defined like it is right now:

($) :: forall (w :: GHC.Types.Levity) a (b :: TYPE w). (a -> b) -> a -> b

But when it is used in a module without levity polymorphism enabled, "w" is defaulted to "Lifted", "b" gets kind "*", and ($) gets its old type:

($) :: (a -> b) -> a -> b

So any use of ($) with types on kind "#" is disallowed.

But with levily polymorphism enabled, one will see the full type and use ($) with unlifted types. To prevent breakage of the existing code, MagicHash extension should by default imply levity polymorphism.

What do you think? Am I missing something?

Thanks, Yuras.

...

* There are further questions regarding the appropriate kinds of (->) and (.) [1]

* Incidentally, there is a GHC or Haddock bug [2] which causes kind signatures to be unnecessarily shown in documentation for some types, exposing levities to the user.

The current plan to address this situation is as follows,

* Introduce [3] a flag, -fshow-runtime-rep, which when disabled will cause the pretty-printer to instantiate levity-polymorphic types as lifted (e.g. resulting in *). This flag will be off by default, meaning that users will in most cases see the usual lifted types unless they explicitly request otherwise.

* Fix the GHC/Haddock bug, restoring elision of unnecessary kind signatures in documentation.

* In the future we should seriously consider introducing an alternate Prelude for beginners

As far as I can tell from the discussion, this was an acceptable solution to all involved. If there are any remaining objections or concerns let's discuss them in another thread.

Thanks to everyone who contributed to this effort.

Cheers,

- Ben

[1] https://ghc.haskell.org/trac/ghc/ticket/10343#comment:27 [2] https://ghc.haskell.org/trac/ghc/ticket/11567 [3] https://ghc.haskell.org/trac/ghc/ticket/11549 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

"Boespflug, Mathieu" writes:

Hi Ben,

thanks for the nice summary. I haven't been following all the details in the meanderings of this thread, but perhaps someone can chime in with an answer to this simple question:

* has it been discussed what type ($) should have in the Haddock's for base? If so, will it the one GHCi shows by default, or the one GHCi will show when -fshow-runtime-rep?

If the former, how is a user supposed to discover that ($) is in fact more general than what the docs would tell you?

If the latter, wouldn't the Haddock's be just as confusing to beginners as GHCi's output currently is? Wouldn't it be even more confusing that the Haddock's and GHCi don't agree about what the type of ($) really is?

Indeed, the disagreement is confusing, but we have been living with this confusion for quite some time now as ($) is already open-kinded. If nothing else, this new state of affairs is slightly better since if you know the secret -fshow-runtime-rep incantation you can convince GHCi to tell you the real type. As far as I know, there is currently know way to do this in 7.10. Given how much backlash there has been to changing the type of ($), I'd be fine not using -fshow-runtime-rep during the core library haddock builds. In effect the message to users would be, "yes, unboxed types exist and they are now on sound theoretical footing, but they are still largely an implementation detail, just as they have always been. If you want to use them you need to know where to look." Perhaps this can be revisited at some point in the future when we have a better story for a beginner's Prelude but for now I'm not sure we want to subject everyone to these new types. Anyways, this is just my two cents. It would be nice to hear what others think. Cheers, - Ben

"Boespflug, Mathieu" writes:

...

As far as I know, there is currently know way to do this in 7.10.

Given how much backlash there has been to changing the type of ($), ...

Keep in mind... as we saw with FTP, that in this community it's often unclear just how large or tiny a group of people represent when they're vocal (could be an outright majority, could in fact be just a handful... hard to tell). ;)

This is very true. I wish we had better instruments for judging consensus. Sadly it seems this is a problem that has long resisted solution.

...

I'd be fine not using -fshow-runtime-rep during the core library haddock builds. In effect the message to users would be,

"yes, unboxed types exist and they are now on sound theoretical footing, but they are still largely an implementation detail, just as they have always been. If you want to use them you need to know where to look."

When that last sentence is expanded out a bit to explain what "know where to look means", it means

"yes, unboxed types exist and they are now on sound theoretical footing [...]. If you want to use them you need to know where to look, i.e. pass -fshow-runtime-types to GHCi every time, and compile your own Haddock's, keep them safe somewhere on your computer and point your browser there instead, because https://downloads.haskell.org/~ghc/latest/docs/html/libraries/ is not going to tell you where you can use it."

All in a laudable effort to present less information to beginners out-of-the-box, IMHO the story is starting to look awefully complicated for Haskell practitioners, i.e. beginners-a-little-while-ago...

Well said.

Said another way, sounds to me like we're in a case of: avoiding surprise now begets bigger surprise later (and wasted time trying to discover all these myriad flags whose sole existence was to pretend to her/him that things are simpler than they really are, and then dealing with their consequences...) when the beginner becomes practitioner.

Sure, but there is a trade-off here. Even in performance-sensitive applications unboxed types don't appear that frequently. Now, perhaps this will change as these types become well-behaved members of the language. However at the moment I'm not convinced that the consistency that showing this polymorphism to all users pays for itself. Afterall, the signatures are significantly noiser than the current monomorphic forms. However, I think we should certainly reconsider this once we have had some experience working with these types in the post-levity-polymorphic world and have worked out how to deal with some of the more human issues that they bring. <aside> At the moment levity-polymorphic types are a fair bit more noisy than their lifted counterparts. I think this is a problem which raises an interesting of information presentation. While reading documentation, I find that I usually read from the right to left. That is, if faced with given foldMap :: forall a m t. (Foldable t, Monoid m) => (a -> m) -> t a -> m My eye will typically follow a trajectory of, 1. start with the binder, `foldMap` 2. look at the shape of the type, `(a -> m) -> t a -> m` 3. refer to the context to see what is demanded of these types 4. look back to the shape, folding in knowledge from the constraints 5. if there are still questions, refer to type variable signatures in the forall clause. 6. repeat 3 through 5 until satisfied Unfortunately it takes a fair amount of visual processing for even a seasoned user to segment the signature into these four pieces. Moreover, the majority of the signature is context and the forall clause, which are arguably the parts that one looks at least. An easy way to counteract this in Haddock would be to remove emphasis from the forall clause (either reduce its contrast or collapse it entirely). In the case of typeclass polymorphism haddock tries to make types easier to grok by presenting specializations of typeclass methods in instance documentation. While I'm not sure that this exact scheme would help much for levity, I wonder what other ideas in this vein we could try. In the case of GHCi, I suspect something like Richard's suggestion of a more interactive console. </aside>

...

Perhaps this can be revisited at some point in the future when we have a better story for a beginner's Prelude but for now I'm not sure we want to subject everyone to these new types.

TBH I'm fairly skeptical about the "Prelude for beginners" idea. Things like e.g. the AMP require that everyone has the same idea of what the definition of the Monad class is. Yet it's not like you're either a beginner or you're not: it's a continuum (we're all beginners, just some less than others...). When beginners start uploading new packages on Hackage (and I hope they do), but do so using BeginnerPrelude because that's what they were taught, then we start having to make the (artificially created) "beginner world" and the "real world" agree. If I define an instance of a BeginnerPrelude class in package A, it might not be exploitable in package B. Worse, if what we're really talking about is beginner-base, then what happens when they both define their own Data.List module? So in the end the scope of a BeginnerPrelude may be very limited indeed.

If a beginner Prelude is really the right way forward, then surely one of the many authors of Haskell books would have put one forward by now and recommend using that?

But perhaps this is a topic for another thread...

Indeed. I'll just say that I envision that a beginner's prelude would be for learning and nothing more. The goal is that it would be used in the first dozen hours of picking up the language and nothing more. I'd be interested to hear what Richard had in mind when he has time again. Cheers, - Ben

Richard Eisenberg :

On Feb 16, 2016, at 5:35 AM, Ben Gamari wrote:

...

Indeed. I'll just say that I envision that a beginner's prelude would be for learning and nothing more. The goal is that it would be used in the first dozen hours of picking up the language and nothing more.

I'd be interested to hear what Richard had in mind when he has time again.

Yes, that's right. And, of course, it doesn't even need to be something released with GHC.

I hope to have the opportunity to teach intro Haskell in the not-too-distant future. Maybe even this coming fall. Though I have yet to look closely at Chris's book, which will be one of the first things I do to prep, I suspect I'll be writing a custom Prelude for my first few weeks of the class, eliminating all type-classes. No Foldable, no Monoid, no Num. And then, by week 3 or 4, bring all that back in.

As somebody who has taught Haskell to hordes of students (literally, 1000s), I am not at all convinced that this is going to be helpful. This is for the following reasons: * Students understand the basic idea of overloading for Num, Show, etc easily (week 1 or 2). We actually tried both doing basic overloading very early or delaying it until later. The former worked much better. * You are not in a position to explain Foldable and probably not Monoid by week 3 or 4. So, either you need to have more than one beginner Prelude, delay overloading until much later (awkward), or we are really only talking about the impact of Show, Num, etc here. * Changing things (i.e., one Prelude to another) always confuses some people — i.e., there is an intellectual cost to all this. * Students will want to use Haskell on their own computers. Then, you need to make sure, they import the right Prelude and that they stop importing the beginner Prelude when you switch back to the normal one. A certain percentage of students will mess that up and be confused. What we found works best is the following: * Introduce the concept of overloading right away. People get that easily, because they use overloaded arithmetic functions in math, too. (Num and Show are the typical classes to explain it at.) As an example, see how we do that in the first chapter of our new Haskell tutorial: http://learn.hfm.io/first_steps.html * Be careful in designing your exercises/assignments (esp early ones), to make it unlikely for students to run into class related errors. Sorry for the mostly off-topic post, but since a beginner’s Prelude was mentioned here multiple times recently as a countermeasure to making the real Prelude more complicated, I just want to say, don’t put too much hope into a ”solution” you never actually tried. Manuel

We have tried variations of this. This approach has two problems. (1) It’s generally easier to use something than to define it and, e.g., in the case of lists, Haskell ”magic” syntax is more intuitive to use. For example, we use lists for a while before we define them. Even recursive definitions with pattern matching on [] and (:) are fairly easy to explain and for students to write quite a while before we discuss data declarations. The build-in syntax for lists is convenient for using collections before properly explaining the full structure of terms and the concept of data constructors etc. (2) We repeatedly found that any for-teaching-only definitions come with quite a bit of hidden costs. At some point, you need to make the transition from the for-teaching-only definitions to the ”real” definitions. At this point, you invariably lose the students who managed to just get everything up to that point — i.e., those students that were struggling anyway. For us, alpha renaming is a trivial process. However, learners (and esp. the weaker learners) are rather tied to syntax and concrete names. They don’t deal well with alpha renaming. Additionally, by introducing for-teaching-only definitions, you basically cut learners of from all the online resources that they could otherwise access. You probably won’t be able to match it up with a textbook unless you write one yourself. (Even if there is a book, this book then becomes the only resource.) This is an enormous disadvantage. Manuel

Joachim Breitner : Am Mittwoch, den 17.02.2016, 10:05 +1100 schrieb Manuel M T Chakravarty:

...

* Be careful in designing your exercises/assignments (esp early ones), to make it unlikely for students to run into class related errors.

have you, or someone else, considered or tried to simply have students start with their own list data type, i.e.

data List a = Nil | Cons a (List a)

and have them implement the combinators they need themselves? Of course, you’d have to tell them to use names that do not clash with Prelude-exported, but this would avoid Foldable et. al. and be more educational (at the expense of maybe a slower progress, and not having nice syntax).

Similarly, one could teach them about the non-magicness of $ and side- step the issue with $ by having them write

($$) :: (a -> b) -> a -> b f $$ x = f x infixr 0 $

(or whatever symbol they fancy).

This would be akin to using a beginner’s prelude, only that the students would be writing it themselves, which IMHO is a big difference from an educational point of view.

Greetings, Joachim

-- Joachim “nomeata” Breitner mail@joachim-breitner.de • https://www.joachim-breitner.de/ XMPP: nomeata@joachim-breitner.de • OpenPGP-Key: 0xF0FBF51F Debian Developer: nomeata@debian.org

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Hi Takenobu,

Takenobu Tani :

Hi Manuel,

...

* Introduce the concept of overloading right away. People get that easily, because they use overloaded arithmetic functions in math, too. (Num and Show are the typical classes to explain it at.) As an example, see how we do that in the first chapter of our new Haskell tutorial: http://learn.hfm.io/first_steps.html http://learn.hfm.io/first_steps.html

This is straightforward and elegance tutorial! I like this.

You are very kind. Thank you.

As you know, I'll share one point to list.

It's better to assume that "beginners are not only students in universities". Beginners are also engineers, hobbyist, teenager, your friends and your family. Someone of them will touch to Haskell alone and learn with self study in a little bit of knowledge.

If they feel complex at first impression in their 1st week, they would go back before they realize beauty of Haskell.

Sometimes, I’m worried about it.

I do worry about the same thing. The Haskell ecosystem is very much geared towards experts and tinkerers (with laudable exceptions, such as, for example, the great work done by Chris Allen). Being an expert and tinkerer that didn’t worry me too much, but lately I am trying to make functional programming and Haskell accessible to a broader audience and it is an uphill battle. Even many professional software developers are put off even trying to install the toolchain. It is not that they wouldn’t been able to do it if they wanted. They just can’t be bothered because they are not convinced of the value of doing so at this stage — exactly as you are saying. We should make it easier to get started, not harder. Manuel

I agree 100% with Manuel here. My N is smaller (100s rather than thousands) but this is what I've seen working with self-learners, programmers and non-programmers alike. I don't have anything further to add because I couldn't find a point in his listing that didn't match my experience.

Sorry for the mostly off-topic post, but since a beginner’s Prelude was mentioned here multiple times recently as a countermeasure to making the real Prelude more complicated, I just want to say, don’t put too much hope into a ”solution” you never actually tried.

I have tried a beginner's Prelude with people. I don't have a lot of data because it was clearly a failure early on so I bailed them out into the usual thing. It's just not worth it and it deprives them of the preparedness to go write real Haskell code. That's not something I'm willing to give up just so I can teach _less_. On Tue, Feb 16, 2016 at 5:05 PM, Manuel M T Chakravarty < chak@justtesting.org> wrote:

...

Richard Eisenberg :

On Feb 16, 2016, at 5:35 AM, Ben Gamari wrote:

...

Indeed. I'll just say that I envision that a beginner's prelude would be for learning and nothing more. The goal is that it would be used in the first dozen hours of picking up the language and nothing more.

I'd be interested to hear what Richard had in mind when he has time again.

Yes, that's right. And, of course, it doesn't even need to be something released with GHC.

I hope to have the opportunity to teach intro Haskell in the not-too-distant future. Maybe even this coming fall. Though I have yet to look closely at Chris's book, which will be one of the first things I do to prep, I suspect I'll be writing a custom Prelude for my first few weeks of the class, eliminating all type-classes. No Foldable, no Monoid, no Num. And then, by week 3 or 4, bring all that back in.

As somebody who has taught Haskell to hordes of students (literally, 1000s), I am not at all convinced that this is going to be helpful. This is for the following reasons:

* Students understand the basic idea of overloading for Num, Show, etc easily (week 1 or 2). We actually tried both doing basic overloading very early or delaying it until later. The former worked much better.

* You are not in a position to explain Foldable and probably not Monoid by week 3 or 4. So, either you need to have more than one beginner Prelude, delay overloading until much later (awkward), or we are really only talking about the impact of Show, Num, etc here.

* Changing things (i.e., one Prelude to another) always confuses some people — i.e., there is an intellectual cost to all this.

* Students will want to use Haskell on their own computers. Then, you need to make sure, they import the right Prelude and that they stop importing the beginner Prelude when you switch back to the normal one. A certain percentage of students will mess that up and be confused.

What we found works best is the following:

* Introduce the concept of overloading right away. People get that easily, because they use overloaded arithmetic functions in math, too. (Num and Show are the typical classes to explain it at.) As an example, see how we do that in the first chapter of our new Haskell tutorial: http://learn.hfm.io/first_steps.html

* Be careful in designing your exercises/assignments (esp early ones), to make it unlikely for students to run into class related errors.

Sorry for the mostly off-topic post, but since a beginner’s Prelude was mentioned here multiple times recently as a countermeasure to making the real Prelude more complicated, I just want to say, don’t put too much hope into a ”solution” you never actually tried.

Manuel

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

On Wed, Feb 17, 2016, at 08:09, Christopher Allen wrote:

I have tried a beginner's Prelude with people. I don't have a lot of data because it was clearly a failure early on so I bailed them out into the usual thing. It's just not worth it and it deprives them of the preparedness to go write real Haskell code. That's not something I'm willing to give up just so I can teach _less_.

Chris, have you written about your experiences teaching with a beginner's Prelude? I'd be quite interested to read about it, as (1) it seems like a natural thing to do and (2) the Racket folks seem to have had good success with their staged teaching languages. In particular, I'm curious if your experience is in the context of teaching people with no experience programming at all, vs programming experience but no Haskell (or generally FP) experience. The Racket "How to Design Programs" curriculum seems very much geared towards absolute beginners, and that could be a relevant distinction. Thanks! Eric

Hi, I know the issue of beginner's Prelude. But how about "profile"? (like H264/MPEG4-AVC profile [1]) * Beginner Profile : beginner's Prelude or ghci beginner's representation mode * Main Profile : Haskell 2010 standard * Leading edge Profile : set of GHC extensions If beginners know exist of profile at first, they may avoid to confuse by step-up? More confused? Already we implicitly have at least two profiles (Haskell2010 and GHC extensions). [1] https://en.wikipedia.org/wiki/H.264/MPEG-4_AVC#Profiles Regards, Takenobu 2016-02-18 16:45 GMT+09:00 Herbert Valerio Riedel :

On 2016-02-18 at 04:02:24 +0100, Eric Seidel wrote:

...

On Wed, Feb 17, 2016, at 08:09, Christopher Allen wrote:

...

I have tried a beginner's Prelude with people. I don't have a lot of data because it was clearly a failure early on so I bailed them out into the usual thing. It's just not worth it and it deprives them of the preparedness to go write real Haskell code. That's not something I'm willing to give up just so I can teach _less_.

Chris, have you written about your experiences teaching with a beginner's Prelude? I'd be quite interested to read about it, as (1) it seems like a natural thing to do and (2) the Racket folks seem to have had good success with their staged teaching languages.

In particular, I'm curious if your experience is in the context of teaching people with no experience programming at all, vs programming experience but no Haskell (or generally FP) experience. The Racket "How to Design Programs" curriculum seems very much geared towards absolute beginners, and that could be a relevant distinction.

Btw, IMHO it's also interesting to distinguish between teaching functional programming vs teaching Haskell.

I've noticed that in the former case, instructors would often prefer a radically slimmed down standard-library and conceal some of Haskell's language features not pertinent to their FP curriculum (e.g. typeclasses or record syntax).

-- _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I dispute your second point a bit: I consider any Prelude changes a standard library change than a language change, not withstanding the fact the Prelude is imported by default. Any beginner-language library can still be imported from normal code. Likewise a "hygienic copy paste" would simply import the beginner prelude qualified and mangle identifiers as necessary. I'm inclined to think the Racket way is the only true solution here. John On Wed, Feb 24, 2016 at 6:07 PM, Manuel M T Chakravarty < chak@justtesting.org> wrote:

Two notable differences between Racket and the situation in Haskell is that (1) Racket has a full blown IDE to support the staged languages and (2) AFIK any Racket program in a simpler language is still a valid Racket program in a more advanced language. (The latter wouldn’t be the case with, e.g., a Prelude omitting type classes as you need to introduce new names —to avoid overloading— that are no longer valid in the full Prelude.)

Manuel

...

Eric Seidel :

On Wed, Feb 17, 2016, at 08:09, Christopher Allen wrote:

...

I have tried a beginner's Prelude with people. I don't have a lot of data because it was clearly a failure early on so I bailed them out into the usual thing. It's just not worth it and it deprives them of the preparedness to go write real Haskell code. That's not something I'm willing to give up just so I can teach _less_.

Chris, have you written about your experiences teaching with a beginner's Prelude? I'd be quite interested to read about it, as (1) it seems like a natural thing to do and (2) the Racket folks seem to have had good success with their staged teaching languages.

In particular, I'm curious if your experience is in the context of teaching people with no experience programming at all, vs programming experience but no Haskell (or generally FP) experience. The Racket "How to Design Programs" curriculum seems very much geared towards absolute beginners, and that could be a relevant distinction.

Thanks! Eric _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Yes, the inference of call-stacks is being removed. I'm just waiting for the patch to be reviewed. On Mon, Mar 28, 2016, at 06:22, George Colpitts wrote:

Was there any consensus on how to move forward on this? I just found another example of ​​ 8.0 type which is not beginner friendly:

bash-3.2$ ghci GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help Prelude> True True it :: Bool Prelude> True || undefined True *it :: ?callStack::GHC.Stack.Types.CallStack => Bool*

On Wed, Mar 2, 2016 at 1:56 PM Ericson, John wrote:

...

I dispute your second point a bit: I consider any Prelude changes a standard library change than a language change, not withstanding the fact the Prelude is imported by default. Any beginner-language library can still be imported from normal code. Likewise a "hygienic copy paste" would simply import the beginner prelude qualified and mangle identifiers as necessary.

I'm inclined to think the Racket way is the only true solution here.

John

On Wed, Feb 24, 2016 at 6:07 PM, Manuel M T Chakravarty < chak@justtesting.org> wrote:

...

Two notable differences between Racket and the situation in Haskell is that (1) Racket has a full blown IDE to support the staged languages and (2) AFIK any Racket program in a simpler language is still a valid Racket program in a more advanced language. (The latter wouldn’t be the case with, e.g., a Prelude omitting type classes as you need to introduce new names —to avoid overloading— that are no longer valid in the full Prelude.)

Manuel

...

Eric Seidel :

On Wed, Feb 17, 2016, at 08:09, Christopher Allen wrote:

...

I have tried a beginner's Prelude with people. I don't have a lot of data because it was clearly a failure early on so I bailed them out into the usual thing. It's just not worth it and it deprives them of the preparedness to go write real Haskell code. That's not something I'm willing to give up just so I can teach _less_.

Chris, have you written about your experiences teaching with a beginner's Prelude? I'd be quite interested to read about it, as (1) it seems like a natural thing to do and (2) the Racket folks seem to have had good success with their staged teaching languages.

In particular, I'm curious if your experience is in the context of teaching people with no experience programming at all, vs programming experience but no Haskell (or generally FP) experience. The Racket "How to Design Programs" curriculum seems very much geared towards absolute beginners, and that could be a relevant distinction.

Thanks! Eric _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I don't think it's a good idea to create a dumbed down Prelude and existing resources not covering what programmers need to know in order to actually use Haskell as everyone else uses it is much of the reason I had to write a book to begin with. This type isn't just noise for beginners, it's noise for practitioners too. Consider what I said earlier about a 15 year user of Haskell finding the type confusing and irrelevant. There are a couple good proposals for addressing levity polymorphism leaking into the type. I think the one Ben Gamari had in mind that I thought would be fine is waiting for a patch. On Mon, Feb 15, 2016 at 6:30 PM, Manuel M T Chakravarty < chak@justtesting.org> wrote:

...

Ben Gamari : builds. In effect the message to users would be,

"yes, unboxed types exist and they are now on sound theoretical footing, but they are still largely an implementation detail, just as they have always been. If you want to use them you need to know where to look."

Perhaps this can be revisited at some point in the future when we have a better story for a beginner's Prelude but for now I'm not sure we want to subject everyone to these new types.

Anyways, this is just my two cents. It would be nice to hear what others think.

Sounds like a good plan to me.

Manuel

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

Thank you for the reply! On Sun, 2016-02-14 at 22:58 -0500, Richard Eisenberg wrote:

This approach wouldn't quite work.

- It seems to kick in only when instantiating a Levity variable. That would not happen when using :info.

Obviously Levity variables should be defaulted to Lifted everywhere, including :info and :type. Is it possible or are there some technical limitations?

- It is possible to have unlifted types about even without -XMagicHash. -XMagicHash is simply a lexer extension, nothing more. By convention, we use the # suffix with unlifted things, but there's no requirement here. Having -XMagicHash thus imply a flag about the type system is bizarre.

OK, I always forget about that. But is not it a bug already? Usually we don't allow code that uses GHC-specific extensions to compile without a language pragma. Why we don't have such pragma for levity polymorphism? If we agree that we need a pragma, then we can find a way to introduce it without massive code breakage, e.g. we can add a warning to -Wcompat and make the pragma mandatory in 3 releases. Then we can have -fshow- runtime-rep as a temporary solution. It naturally solves an issue with Haddock -- it should show levity polymorphic type when an identifier is exported from a module with the pragma, and monomorphic type otherwise. Basically that is what haddock does for KindSignatures.

Furthermore, I'm not sure what the practical, user-visible improvement would be over the approach you include and the -fshow- runtime-rep idea.

The improvement is to keep ($) type as specified by Haskell2010 report (including :info) and never lie about it, but allow levity polymorphism when explicitly requested by user.

Richard

On Feb 13, 2016, at 11:40 AM, Yuras Shumovich wrote:

...

Thank you for the summary! The thread is too big to find anything in it.

I'd like to present a bit different approach, kind of a compromise, without lie and code breakage: introduce a language pragma for levity polymorphism and default levity polymorphic signatures to "*" when the pragma is not enabled.

For example, ($) could be defined like it is right now:

($)   :: forall (w :: GHC.Types.Levity) a (b :: TYPE w).      (a -> b) -> a -> b

But when it is used in a module without levity polymorphism enabled, "w" is defaulted to "Lifted", "b" gets kind "*", and ($) gets its old type:

($)   :: (a -> b) -> a -> b

So any use of ($) with types on kind "#" is disallowed.

But with levily polymorphism enabled, one will see the full type and use ($) with unlifted types. To prevent breakage of the existing code, MagicHash extension should by default imply levity polymorphism.

What do you think? Am I missing something?

Thanks, Yuras.

...

 * There are further questions regarding the appropriate kinds    of (->) and (.) [1]

 * Incidentally, there is a GHC or Haddock bug [2] which causes kind    signatures to be unnecessarily shown in documentation for some types,    exposing levities to the user.

The current plan to address this situation is as follows,

 * Introduce [3] a flag, -fshow-runtime-rep, which when disabled will    cause the pretty-printer to instantiate levity-polymorphic types as    lifted (e.g. resulting in *). This flag will be off by default,    meaning that users will in most cases see the usual lifted types    unless they explicitly request otherwise.

 * Fix the GHC/Haddock bug, restoring elision of unnecessary kind    signatures in documentation.

 * In the future we should seriously consider introducing an alternate    Prelude for beginners   As far as I can tell from the discussion, this was an acceptable solution to all involved. If there are any remaining objections or concerns let's discuss them in another thread.

Thanks to everyone who contributed to this effort.

Cheers,

- Ben

[1] https://ghc.haskell.org/trac/ghc/ticket/10343#comment:27 [2] https://ghc.haskell.org/trac/ghc/ticket/11567 [3] https://ghc.haskell.org/trac/ghc/ticket/11549 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On 2016-02-15 at 12:00:23 +0100, Yuras Shumovich wrote: [...]

...

- It is possible to have unlifted types about even without -XMagicHash. -XMagicHash is simply a lexer extension, nothing more. By convention, we use the # suffix with unlifted things, but there's no requirement here. Having -XMagicHash thus imply a flag about the type system is bizarre.

OK, I always forget about that. But is not it a bug already? Usually we don't allow code that uses GHC-specific extensions to compile without a language pragma. Why we don't have such pragma for levity polymorphism?

There are extensions which are only needed at the definition site. Take {-# LANGUAGE PolyKinds #-} for instance; this is enabled inside the Data.Proxy module, which defines the following type {-# LANGUAGE PolyKinds #-} module Data.Proxy where data Proxy t = Proxy Now when you query via GHCi 7.10, you get the following output

import Data.Proxy :i Proxy type role Proxy phantom data Proxy (t :: k) = Proxy -- Defined in ‘Data.Proxy’ instance forall (k :: BOX) (s :: k). Bounded (Proxy s) -- Defined in ‘Data.Proxy’ instance forall (k :: BOX) (s :: k). Enum (Proxy s) -- Defined in ‘Data.Proxy’ instance forall (k :: BOX) (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’ instance Monad Proxy -- Defined in ‘Data.Proxy’ instance Functor Proxy -- Defined in ‘Data.Proxy’ instance forall (k :: BOX) (s :: k). Ord (Proxy s) -- Defined in ‘Data.Proxy’ instance forall (k :: BOX) (s :: k). Read (Proxy s) -- Defined in ‘Data.Proxy’ instance forall (k :: BOX) (s :: k). Show (Proxy s) -- Defined in ‘Data.Proxy’ instance Applicative Proxy -- Defined in ‘Data.Proxy’ instance Foldable Proxy -- Defined in ‘Data.Foldable’ instance Traversable Proxy -- Defined in ‘Data.Traversable’ instance forall (k :: BOX) (s :: k). Monoid (Proxy s) -- Defined in ‘Data.Proxy’

even though you never enabled any extensions beyond what Haskell2010 provides. Do you consider this a bug as well?

Ah, and I offer my help in case development efforts is the main concern. Though I'm not familiar with this part of GHC, so I'd need a mentor. My help probably will not be very useful, but I'd be happy to participate. On Mon, 2016-02-15 at 15:21 +0300, Yuras Shumovich wrote:

On Mon, 2016-02-15 at 12:35 +0100, Herbert Valerio Riedel wrote:

...

On 2016-02-15 at 12:00:23 +0100, Yuras Shumovich wrote:

[...]

...

...

- It is possible to have unlifted types about even without -XMagicHash. -XMagicHash is simply a lexer extension, nothing more. By convention, we use the # suffix with unlifted things, but there's no requirement here. Having -XMagicHash thus imply a flag about the type system is bizarre.

OK, I always forget about that. But is not it a bug already? Usually we don't allow code that uses GHC-specific extensions to compile without a language pragma. Why we don't have such pragma for levity polymorphism?

There are extensions which are only needed at the definition site. Take {-# LANGUAGE PolyKinds #-} for instance; this is enabled inside the Data.Proxy module, which defines the following type

  {-# LANGUAGE PolyKinds #-}   module Data.Proxy where

  data Proxy t = Proxy

Now when you query via GHCi 7.10, you get the following output

  > import Data.Proxy   > :i Proxy    type role Proxy phantom   data Proxy (t :: k) = Proxy      -- Defined in ‘Data.Proxy’   instance forall (k :: BOX) (s :: k). Bounded (Proxy s) -- Defined in ‘Data.Proxy’   instance forall (k :: BOX) (s :: k). Enum (Proxy s) -- Defined in ‘Data.Proxy’   instance forall (k :: BOX) (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’   instance Monad Proxy -- Defined in ‘Data.Proxy’   instance Functor Proxy -- Defined in ‘Data.Proxy’   instance forall (k :: BOX) (s :: k). Ord (Proxy s) -- Defined in ‘Data.Proxy’   instance forall (k :: BOX) (s :: k). Read (Proxy s) -- Defined in ‘Data.Proxy’   instance forall (k :: BOX) (s :: k). Show (Proxy s) -- Defined in ‘Data.Proxy’   instance Applicative Proxy -- Defined in ‘Data.Proxy’   instance Foldable Proxy -- Defined in ‘Data.Foldable’   instance Traversable Proxy -- Defined in ‘Data.Traversable’   instance forall (k :: BOX) (s :: k). Monoid (Proxy s) -- Defined in ‘Data.Proxy’

even though you never enabled any extensions beyond what Haskell2010 provides.

Do you consider this a bug as well?

Yes, IMO it is a bug. Though people didn't complain so far, so lets say it is a minor design flow. Probably there are more important bugs to fix.

Ideally language extensions should not leak to Haskell2010. E.g. making lens using TemplateHaskell doens't leak to use side because I can define lens by hands and preserve the API. But if something can't be expressed in Haskell2010, then it should require extension to be enabled both of definition and use sides.

In case of ($) people complain, and everybody seem to agree that levity polymorphism leaking to Haskell2010 is bad. Fixing the leakage IMO is the right way, while hiding the issue behind -fshow-rutime-rep is a hack and a lie.

Probably the right way is harder in terms of development efforts (I have no idea). In that case it probably makes sense to choose easier way and introduce a hack. Life consists of compromises.