[GHC] #12540: RFC: Allow not quantifying every top-level quantifiee
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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: -------------------------------------+------------------------------------- Minor nuisance, does this happen to anyone else? Currently Haskell has an all-nothing policy on quantified type variables, either you quantify none or all (fine, let's ignore non-prenex quantification `foo :: a -> forall b. b -> a`). Can we have a top-level quantification of only a subset of the free variables? Say I'm working on a function {{{#!hs reflected :: forall s m a. (Applicative m, Reifies s a) => TaggedT s m a }}} and I need to make ''s'' a scoped type variable, I always accidentally write {{{#!hs reflected :: forall s. (Applicative m, Reifies s a) => TaggedT s m a reflected = TagT . pure . reflect $ (Proxy :: Proxy s) }}} This causes GHC to complain that the other types — ''m'', ''a'' — are not in scope so and I have to add the remaining quantifiees I don't really care about (may have long names as well). It could be worse (''dramatization'') {{{#!hs ipartsOf :: forall i p f s t a. (Indexable [i] p, Functor f) => Traversing (Indexed i) f s t a a -> Over p f s t [a] [a] ipartsOf l = conjoined (\f s -> let b = inline l sell s in outs b <$> f (wins b)) (\f s -> let b = inline l sell s; (is, as) = unzip (pins b) in outs b <$> indexed f (is :: [i]) as) appendAssocAxiom :: forall p q r as bs cs. p as -> q bs -> r cs -> Dict ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs)) appendAssocAxiom _ _ _ = unsafeCoerce (Dict :: Dict (as ~ as)) }}} It would be nice to be nice to only have to specify the type one is interested in: {{{#!hs ipartsOf :: forall i. (Indexable [i] p, Functor f) => Traversing (Indexed i) f s t a a -> Over p f s t [a] [a] appendAssocAxiom :: forall as. p as -> q bs -> r cs -> Dict ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs)) }}} and have the others chosen in some way. This is not just useful for writing, but it makes it easier to read: If I see a type `forall i p f s t a. ...` any of them may appear in the function body, if I see a type `forall i. ...` I know only one is. Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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 mpickering): I also regularly do this! Seems like a sensible suggestion to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -11,1 +11,1 @@ - reflected :: forall s m a. (Applicative m, Reifies s a) => TaggedT s m a + reflected :: (Applicative m, Reifies s a) => TaggedT s m a New description: Minor nuisance, does this happen to anyone else? Currently Haskell has an all-nothing policy on quantified type variables, either you quantify none or all (fine, let's ignore non-prenex quantification `foo :: a -> forall b. b -> a`). Can we have a top-level quantification of only a subset of the free variables? Say I'm working on a function {{{#!hs reflected :: (Applicative m, Reifies s a) => TaggedT s m a }}} and I need to make ''s'' a scoped type variable, I always accidentally write {{{#!hs reflected :: forall s. (Applicative m, Reifies s a) => TaggedT s m a reflected = TagT . pure . reflect $ (Proxy :: Proxy s) }}} This causes GHC to complain that the other types — ''m'', ''a'' — are not in scope so and I have to add the remaining quantifiees I don't really care about (may have long names as well). It could be worse (''dramatization'') {{{#!hs ipartsOf :: forall i p f s t a. (Indexable [i] p, Functor f) => Traversing (Indexed i) f s t a a -> Over p f s t [a] [a] ipartsOf l = conjoined (\f s -> let b = inline l sell s in outs b <$> f (wins b)) (\f s -> let b = inline l sell s; (is, as) = unzip (pins b) in outs b <$> indexed f (is :: [i]) as) appendAssocAxiom :: forall p q r as bs cs. p as -> q bs -> r cs -> Dict ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs)) appendAssocAxiom _ _ _ = unsafeCoerce (Dict :: Dict (as ~ as)) }}} It would be nice to be nice to only have to specify the type one is interested in: {{{#!hs ipartsOf :: forall i. (Indexable [i] p, Functor f) => Traversing (Indexed i) f s t a a -> Over p f s t [a] [a] appendAssocAxiom :: forall as. p as -> q bs -> r cs -> Dict ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs)) }}} and have the others chosen in some way. This is not just useful for writing, but it makes it easier to read: If I see a type `forall i p f s t a. ...` any of them may appear in the function body, if I see a type `forall i. ...` I know only one is. Thoughts? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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 simonpj): I've often wondered about this too. We could simply change the behaviour to always over quantify over un- mentioned tyvars. That gives * Same behaviour when no `forall` * Same behaviour when you specify all variables * But accepts some extra programs. Adding a flag to control it seems overkill. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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 Iceland_jack): Ah that would do just fine, the only downside is that it makes it less explicit if a type variable is scoped (seeing a top-level `forall` is a decent indicator that something in the body needs it) but it sounds good to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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 Iceland_jack): (Example that tripped me up) I wanted to define a `Proxy`-less version of [https://hackage.haskell.org/package/generics-sop-0.2.2.0/docs/Generics- SOP-Classes.html#v:hcpure hcpure]. By muscle memory I quantified over the type variables in the context but the rest.. {{{#!hs hcpure_ :: forall h c xs. (HPure h, AllN h c xs) => (forall (a :: k). c a => f a) -> h f xs hcpure_ = hcpure (Proxy @c) }}} I read my types in linear order: Do I quantify over `a`? (''no'', it's higher rank) Do I quantify over `k`? (''optional'', must appear before `h`, `c` and `f` though). Do I quantify over `c`? (''never mind'' already did) Do I quantify over `f`? (''yes'') Did I do `h`, `f`, `xs` already? This is more analysis than my brain can do quickly :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14245 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: => #14245 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14245 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm not sure I'd like to give up the `forall`-or-nothing rule. But note that there //is// a workaround here: just use extra parentheses: {{{#!hs const_ :: (forall a. a -> b -> a) const_ = const }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14245 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): That's cute but doesn't bring `a` into scope in the function body. This is surprising behavior for parentheses! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14245 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): It's not surprising at all, if you look at it from a certain perspective. After all, in this function: {{{#!hs f :: (forall a. Proxy b -> a -> a) -> Int -> Int f g x = g Proxy x }}} Despite the fact that there's a `forall` in front of `Proxy b -> a -> a`, GHC doesn't complain that `b` is out of scope. That's because the `forall `-or-nothing rule only applies to `forall`s at the top level, which `forall a. Proxy b -> a -> a` is not. That's why `const_ :: (forall a. a -> b -> a)` is accepted, since the `forall` is similarly not at the top level. It's also why this variation is accepted: {{{#!hs const__ :: () => forall a. a -> b -> a const__ = const }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12540: RFC: Allow not quantifying every top-level quantifiee -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14245 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This behavior of parentheses is awful, in my view. Redundant parentheses should never have any impact. (Yes, yes, I know: that statement is a tautology, as it's essentially the definition for "redundant". But I choose to define "redundant" to mean parentheses that are not needed to disambiguate / alter the precedence of operators.) In my opinion, this example shows why the current setup with scoped type variables is a small misdesign. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12540#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC