Opened 3 years ago

Last modified 2 years ago

#12989 new bug

($) can have a more general type

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The documentation (in section 9.12.1 for GHC 8; I don't know what section it is in 8.2) suggests a hypothetical type for ($):

bad :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
              (a :: TYPE r1) (b :: TYPE r2).
       (a -> b) -> a -> b
bad f x = f x

It explains, correctly, that this definition will not work because x has a representation-polymorphic type. However, this doesn't actually explain why ($) doesn't have that type! Indeed, both GHC 8 and 8.2 accept the following:

good :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
              (a :: TYPE r1) (b :: TYPE r2).
       (a -> b) -> a -> b
good f = f

This has very slightly different semantics, but anyone relying on the difference is already doing something they shouldn't. It may or may not be possible to retain the current semantics with some care and magic, if we so desire.

I didn't really know how to characterize this ticket properly. It could be considered a documentation bug or a compiler feature request.

Change History (4)

comment:1 Changed 3 years ago by dfeuer

I think most likely there isn't any way to change the arity magically, so if we want to change the type, we probably have to accept the (small) semantic change.

comment:2 Changed 3 years ago by rwbarton

I don't know whether this would be kosher, but one possibility would be to skip the kind check on arg1_ty in the type checker special case for arg1 $ arg2 and then rewrite the expression into arg1 `good` arg2. (Or for that matter, into a direct application arg1 arg2.) That would never change semantics because it only applies to a saturated application of ($) in the first place.

You still wouldn't be able to use ($) with unboxed argument type in a higher-order context, but at least you would be able to write things like I# $ x# +# y +# z#.

comment:3 Changed 3 years ago by simonpj

Keywords: LevityPolymorphism added

Worth reading our levity polymorphism paper.

good is OK because no value of type a is manipulated by the code for good (see the paper). NB: care is needed during optimisation: eta expansion (to get bad) is not allowed.

So, yes, perhaps ($) could be defied like good, as an arity-1 function. Then it could have the more generous type.

I'll add this to the levity-polymorphism pile; see LevityPolymorphism

comment:4 Changed 2 years ago by andrewthad

One drawback of giving ($) the more general type is than (&) can no longer be made symmetric with it. That is, we have no way of writing:

(&) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
              (a :: TYPE r1) (b :: TYPE r2).
       a -> (a -> b) -> b

This probably isn't that big of a deal, but it is a little weird.

Note: See TracTickets for help on using tickets.