Proposal: simplify type of ($)

[David Feuer]

I am curious about one thing, though. With the single-argument ($),
the type problem is that we need to instantiate a type variable to a type like
(forall s. ST s t) -> t. The type quantification there is wrapped up under the
arrow, rather than being exposed (as it would be in the second argument of
a two-argument ($)). Would allowing such instantiations cause as much trouble
for type inference as general impredicative types?

On Thu, Dec 28, 2017 at 5:26 PM, Edward Kmett <ekmett at gmail.com> wrote:
> This doesn't seem to eliminate the need for the GHC type checking hack.
>
> You still have to instantiate the type of the single argument to ($) with a
> polytype to typecheck the usual runST $ do ... idiom.
>
> Prelude Control.Monad.ST> runST $ pure ()
>
> ()
>
> Prelude Control.Monad.ST> let ($) a = a
>
> Prelude Control.Monad.ST> runST $ pure ()
>
>
> <interactive>:4:1: error:
>
>     • Couldn't match type ‘forall s. ST s t’ with ‘f0 ()’
>
>       Expected type: f0 () -> t
>
>         Actual type: (forall s. ST s t) -> t
>
>     • In the first argument of ‘($)’, namely ‘runST’
>
>       In the expression: runST $ pure ()
>
>       In an equation for ‘it’: it = runST $ pure ()
>
>     • Relevant bindings include it :: t (bound at <interactive>:4:1)
>
>
>
> -Edward
>
> On Thu, Dec 28, 2017 at 12:59 PM, David Feuer <david.feuer at gmail.com> wrote:
>>
>> It's still a binary operator syntactically. The negation operator is an
>> entirely different kettle of fish.
>>
>> On Dec 28, 2017 11:59 AM, "Jeffrey Brown" <jeffbrown.the at gmail.com> wrote:
>>>
>>> The Wiki says in a few places that Haskell only has one unary operator,
>>> negation. those spots would need updating.
>>>
>>> On Thu, Dec 28, 2017 at 8:04 AM, Ryan Trinkle <ryan.trinkle at gmail.com>
>>> wrote:
>>>>
>>>> Agreed.  I've always taught ($) as "a parenthesis that goes as far
>>>> forward as it can".  That seems to be a pretty good heuristic for people to
>>>> use, and it's a whole lot easier than explaining operator precedence in
>>>> enough detail that the behavior becomes clear from first principles.
>>>>
>>>> On Wed, Dec 27, 2017 at 9:39 PM, Theodore Lief Gannon <tanuki at gmail.com>
>>>> wrote:
>>>>>
>>>>> So far as pedagogy is concerned, ($) is already one of those things
>>>>> people tend to learn how to use before they really understand the mechanism.
>>>>> And for my part, I think if it were immediately obvious that it's just infix
>>>>> id, it would have helped my early understanding of id! +1 from the peanut
>>>>> gallery.
>>>>>
>>>>> On Dec 27, 2017 6:17 PM, "David Feuer" <david.feuer at gmail.com> wrote:
>>>>>>
>>>>>> Currently, we have something like
>>>>>>
>>>>>>     ($) :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2).
>>>>>>       (a -> b) -> a -> b
>>>>>>     f $ x = f x
>>>>>>
>>>>>> And that's only part of the story: GHC has a hack in the type checker
>>>>>> to give ($) an impredicative type when fully applied. This allows it to be
>>>>>> used when its function argument requires a polymorphic argument.
>>>>>>
>>>>>> This whole complicated situation could be resolved in a very simple
>>>>>> manner: change the type and definition thus.
>>>>>>
>>>>>>     ($) :: a -> a
>>>>>>     ($) f = f
>>>>>>
>>>>>> All the type complications go away altogether, and ($) becomes plain
>>>>>> Haskell 98.
>>>>>>
>>>>>> There are only three potential downsides I can think of:
>>>>>>
>>>>>> 1. The optimizer will see `($) x` as fully applied, which could change
>>>>>> its behavior in some cases. There might be circumstances where that is bad.
>>>>>> I doubt there will be many.
>>>>>>
>>>>>> 2. The new type signature may obscure the purpose of the operator to
>>>>>> beginners. But based on my experience on StackOverflow, it seems beginners
>>>>>> tend to struggle with the idea of ($) anyway; this may not make it much
>>>>>> worse. I suspect good Haddocks will help alleviate this concern.
>>>>>>
>>>>>> 3. Some type family and class instances may not be resolved under
>>>>>> certain circumstances which I suspect occur very rarely in practice.
>>>>>>
>>>>>>     class C a where
>>>>>>       m :: (a -> a) -> ()
>>>>>>     instance C (a -> b) where
>>>>>>       m _ = ()
>>>>>>     test :: ()
>>>>>>     test = m ($)
>>>>>>
>>>>>> Today, this compiles with no difficulties; with the proposed change,
>>>>>> the user would have to supply a type signature to make it work:
>>>>>>
>>>>>>     test = m (($) :: (a -> b) -> (a -> b))
>>>>>>
>>>>>> This can also change when an INCOHERENT instance is selected under
>>>>>> similarly contrived circumstances, but those who use such generally deserve
>>>>>> what they get.
>>>>>>
>>>>>> David
>>>>>>
>>>>>> _______________________________________________
>>>>>> Libraries mailing list
>>>>>> Libraries at haskell.org
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> Libraries mailing list
>>>>> Libraries at haskell.org
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> Libraries mailing list
>>>> Libraries at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>
>>>
>>>
>>>
>>> --
>>> Jeff Brown | Jeffrey Benjamin Brown
>>> Website   |   Facebook   |   LinkedIn(spammy, so I often miss messages
>>> here)   |   Github
>>>
>>> _______________________________________________
>>> Libraries mailing list
>>> Libraries at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>