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

Fri Feb 5 16:36:32 UTC 2016

I have a side question and some possible alternate views on a couple things.

The first is: is the fancy type of ($) actually used? It has additional
special type checking behavior that isn't captured in that type
(impredicative instantiation), but probably in a separate code path. Does
that only happen when it's saturated or something, and this is for partial
applications?

Second, it seems like () being overloaded is exactly like type classes, and
(->) is less clearly in that camp (it seems more like a gadt). Just, we
don't have classes at the level necessary to handle ().

-- Dan
On Feb 5, 2016 8:49 AM, "Richard Eisenberg" <eir at cis.upenn.edu> wrote:

> As the instigator of these most recent changes:
>
> - Yes, absolutely, ($)'s type is quite ugly. In other areas, I've tried to
> hide the newfound complexity in the type system behind flags, but I missed
> this one. I consider the current output to be a bug.
>
> - It's conceivable to have a flag -fdefault-levity, on by default, which
> looks for levity polymorphism while printing and instantiates all levity
> variables to Lifted before printing. That would fix the type of ($). Of
> course, users could specify -fno-default-levity. Would this make you happy?
>
> - There's a real drawback to flags like -fdefault-levity (and, relatedly,
> -fprint-explicit-kinds, -fprint-explicit-foralls,
> -fprint-explicit-coercions, -fprint-equality-relations; the last two are
> new in 8.0): they hide things from unsuspecting users. We already get a
> steady trickle of bug reports stemming from confusion around hidden kinds.
> Users diligently try to make a minimal test case and then someone has to
> point out that the user is wrong. It's a waste of time and, I'm sure, is
> frustrating for users. I'm worried about this problem getting worse.
>
> - It's interesting that the solution to the two problems Takenobu pulls
> out below (but others have hinted at in this thread) is by having an
> alternate Prelude for beginners. I believe that having an alternate
> beginners' Prelude is becoming essential. I know I'm not the first one to
> suggest this, but a great many issues that teachers of Haskell have raised
> with me and posts on this and other lists would be solved by an alternate
> Prelude for beginners.
>
> - Separate from a full alternate Prelude, and as Iavor suggested, we could
> just have two ($) operators: a simple one with no baked-in magic or levity
> polymorphism, and then a levity-polymorphic, sneakily impredicative one.
> This would be dead easy.
>
> - Edward is right in that (->) isn't really levity-polymorphic. Well, it
> is, but it's ad hoc polymorphism not parametric polymorphism. Perhaps in
> the future we'll make this more robust by actually using type-classes to
> control it, as we probably should.
>
> - The case with (->) is different than that with (). (() :: Constraint)
> and (() :: *) are wholly unrelated types. () is not
> constraintyness-polymorphic. It's just that we have two wholly unrelated
> types that happen to share a spelling. So there are hacks in the compiler
> to disambiguate. Sometimes these hacks do the wrong thing. If we had
> type-directed name resolution (which I'm not proposing to have!), this
> would get resolved nicely.
>
> - The reason that the foralls get printed in ($)'s type is that kind
> variables appear in the type variables' kinds. GHC thinks that printing the
> foralls are useful in this case and does so without a flag. This is not
> directly related to the levity piece. If you say `:t Proxy`, you'll get
> similar behavior.
>
>
> Bottom line: We *need* an alternate Prelude. But that won't happen for
> 8.0. So in the meantime, I propose -fdefault-levity, awaiting your approval.
>
> Richard
>
> On Feb 5, 2016, at 8:16 AM, Takenobu Tani <takenobu.hs at gmail.com> 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 <mail at joachim-breitner.de>:
>
>> 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 at joachim-breitner.de • http://www.joachim-breitner.de/
>>   Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0xF0FBF51F
>>   Debian Developer: nomeata at debian.org
>>
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160205/bcdadd9c/attachment-0001.html>