[GHC] #12989: ($) can have a more general type
#12989: ($) can have a more general type -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 `($)`: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12989 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12989: ($) can have a more general type -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12989#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12989: ($) can have a more general type -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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#`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12989#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12989: ($) can have a more general type -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => LevityPolymorphism Comment: Worth reading our [https://www.microsoft.com/en-us/research/publication /levity-polymorphism/ 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 [wiki:LevityPolymorphism] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12989#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12989: ($) can have a more general type -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12989#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC