<div dir="ltr">Note: (->) is a type. ($) is a term.<div><br></div><div>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. </div><div><br></div><div>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.</div><div><div><br>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.</div></div><div><br></div><div>($) and other truly levity polymorphic functions are fortunate in that they don't need any such magic hacks and don't care.</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 4, 2016 at 2:53 PM, Christopher Allen <span dir="ltr"><<a href="mailto:cma@bitemyapp.com" target="_blank">cma@bitemyapp.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">My understanding was that the implicitly polymorphic levity, did (->) not change because it's a type constructor?<div><br></div><div><div>Prelude> :info (->)</div><div>data (->) a b <span style="white-space:pre-wrap">     </span>-- Defined in ‘GHC.Prim’</div></div><div><div>Prelude> :k (->)</div><div>(->) :: * -> * -> *</div></div><div><br></div><div>Basically I'm asking why ($) changed and (->) did not when (->) had similar properties WRT * and #.</div><div><br></div><div>Also does this encapsulate the implicit impredicativity of ($) for making runST $ work? I don't presently see how it would.</div><div><br></div><div>Worry not about the book, we already hand-wave FTP effectively. One more type shouldn't change much.</div><div><br></div><div>Thank you very much for answering, this has been very helpful already :)</div><div><br></div><div>--- Chris</div><div><br></div></div><div class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">On Thu, Feb 4, 2016 at 12:52 PM, Ryan Scott <span dir="ltr"><<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Chris,<br>
<br>
The change to ($)'s type is indeed intentional. The short answer is<br>
that ($)'s type prior to GHC 8.0 was lying a little bit. If you<br>
defined something like this:<br>
<br>
    unwrapInt :: Int -> Int#<br>
    unwrapInt (I# i) = i<br>
<br>
You could write an expression like (unwrapInt $ 42), and it would<br>
typecheck. But that technically shouldn't be happening, since ($) ::<br>
(a -> b) -> a -> b, and we all know that polymorphic types have to<br>
live in kind *. But if you look at unwrapInt :: Int -> Int#, the type<br>
Int# certainly doesn't live in *. So why is this happening?<br>
<br>
The long answer is that prior to GHC 8.0, in the type signature ($) ::<br>
(a -> b) -> a -> b, b actually wasn't in kind *, but rather OpenKind.<br>
OpenKind is an awful hack that allows both lifted (kind *) and<br>
unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42)<br>
typechecks. To get rid of the hackiness of OpenKind, Richard Eisenberg<br>
extended the type system with levity polymorphism [1] to indicate in<br>
the type signature where these kind of scenarios are happening.<br>
<br>
So in the "new" type signature for ($):<br>
<br>
    ($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b<br>
<br>
The type b can either live in kind * (which is now a synonym for TYPE<br>
'Lifted) or kind # (which is a synonym for TYPE 'Unlifted), which is<br>
indicated by the fact that TYPE w is polymorphic in its levity type w.<br>
<br>
Truth be told, there aren't that many Haskell functions that actually<br>
levity polymorphic, since normally having an argument type that could<br>
live in either * or # would wreak havoc with the RTS (otherwise, how<br>
would it know if it's dealing with a pointer or a value on the<br>
stack?). But as it turns out, it's perfectly okay to have a levity<br>
polymorphic type in a non-argument position [2]. Indeed, in the few<br>
levity polymorphic functions that I can think of:<br>
<br>
    ($)        :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b<br>
    error     :: forall (v :: Levity)  (a :: TYPE v). HasCallStack =><br>
[Char] -> a<br>
    undefined :: forall (v :: Levity) (a :: TYPE v). HasCallStack => a<br>
<br>
The levity polymorphic type never appears directly to the left of an arrow.<br>
<br>
The downside of all this is, of course, that the type signature of ($)<br>
might look a lot scarier to beginners. I'm not sure how you'd want to<br>
deal with this, but for 99% of most use cases, it's okay to lie and<br>
state that ($) :: (a -> b) -> a -> b. You might have to include a<br>
disclaimer that if they type :t ($) into GHCi, they should be prepared<br>
for some extra information!<br>
<br>
Ryan S.<br>
-----<br>
[1] <a href="https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds</a><br>
[2] <a href="https://ghc.haskell.org/trac/ghc/ticket/11473" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/11473</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div><br><br clear="all"><div><br></div></div></div><span class="HOEnZb"><font color="#888888">-- <br><div><div dir="ltr"><div><div dir="ltr"><div dir="ltr">Chris Allen<br><div><span style="font-size:12.8000001907349px">Currently working on </span><a href="http://haskellbook.com" target="_blank">http://haskellbook.com</a></div></div></div></div></div></div>
</font></span></div>
<br>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
<br></blockquote></div><br></div>