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 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 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 Hi Chris, The change to ($)'s type is indeed intentional. The short answer is
that ($)'s type prior to GHC 8.0 was lying a little bit. If you
defined something like this: unwrapInt :: Int -> Int#
unwrapInt (I# i) = i You could write an expression like (unwrapInt $ 42), and it would
typecheck. But that technically shouldn't be happening, since ($) ::
(a -> b) -> a -> b, and we all know that polymorphic types have to
live in kind *. But if you look at unwrapInt :: Int -> Int#, the type
Int# certainly doesn't live in *. So why is this happening? The long answer is that prior to GHC 8.0, in the type signature ($) ::
(a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind.
OpenKind is an awful hack that allows both lifted (kind *) and
unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42)
typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg
extended the type system with levity polymorphism [1] to indicate in
the type signature where these kind of scenarios are happening. So in the "new" type signature for ($): ($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b The type b can either live in kind * (which is now a synonym for TYPE
'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is
indicated by the fact that TYPE w is polymorphic in its levity type w. Truth be told, there aren't that many Haskell functions that actually
levity polymorphic, since normally having an argument type that could
live in either * or # would wreak havoc with the RTS (otherwise, how
would it know if it's dealing with a pointer or a value on the
stack?). But as it turns out, it's perfectly okay to have a levity
polymorphic type in a non-argument position [2]. Indeed, in the few
levity polymorphic functions that I can think of: ($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b error :: forall (v :: Levity) (a :: TYPE v). HasCallStack =>
[Char] -> a
undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a The levity polymorphic type never appears directly to the left of an
arrow. The downside of all this is, of course, that the type signature of ($)
might look a lot scarier to beginners. I'm not sure how you'd want to
deal with this, but for 99% of most use cases, it's okay to lie and
state that ($) :: (a -> b) -> a -> b. You might have to include a
disclaimer that if they type :t ($) into GHCi, they should be prepared
for some extra information! Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds
[2] https://ghc.haskell.org/trac/ghc/ticket/11473
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs --
Chris Allen
Currently working on http://haskellbook.com ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs --
Chris Allen
Currently working on http://haskellbook.com