[GHC] #10794: Extension request: "where" clauses in type signatures
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature | Status: new request | Priority: lowest | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Some type signatures could be simplified by separating certain elements, either because they are lengthy and can be expressed simpler, to better express intention, or because they are repetitive. A "WhereSignatures" extension would allow for type signatures like the following: {{{#!hs fold :: f -> [a] -> a where f :: a -> a -> a -- expresses intention more clearly than: fold :: (a -> a -> a) -> [a] -> a union :: a -> a -> a where a :: Map.Map k v -- much shorter/more readable than: union :: Map.Map k v -> Map.Map k v -> Map.Map k v }}} Or maybe even: {{{#!hs fmap :: (a -> b) -> f a -> f b where (Functor f) -- arguably prettier than: fmap :: (Functor f) => (a -> b) -> f a -> f b }}} This minor syntactic sugar is essentially equivalent to local "type" definitions, which provides an advantage of making the type's purpose more clear. This seems like a natural development on what the type checker can do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by nomeata): {{{#!hs fold :: f -> [a] -> a where f :: a -> a -> a }}} is certainly confusing, because in the first line `f` is used like a type, but in the second, `f` is used like a value (or `a -> a -> a` is used like a kind Maybe you meant {{{#!hs fold :: f -> [a] -> a where f = a -> a -> a }}} which could be extended to allow {{{#!hs fold :: f -> [a] -> a where f :: * f = a -> a -> a }}} I’m sure the type level programming wizards and dependently typed programmers will have the greatest need for such an extension, and have a good opinion here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by danso: Old description:
Some type signatures could be simplified by separating certain elements, either because they are lengthy and can be expressed simpler, to better express intention, or because they are repetitive. A "WhereSignatures" extension would allow for type signatures like the following:
{{{#!hs fold :: f -> [a] -> a where f :: a -> a -> a
-- expresses intention more clearly than: fold :: (a -> a -> a) -> [a] -> a
union :: a -> a -> a where a :: Map.Map k v
-- much shorter/more readable than: union :: Map.Map k v -> Map.Map k v -> Map.Map k v }}}
Or maybe even:
{{{#!hs fmap :: (a -> b) -> f a -> f b where (Functor f)
-- arguably prettier than: fmap :: (Functor f) => (a -> b) -> f a -> f b }}}
This minor syntactic sugar is essentially equivalent to local "type" definitions, which provides an advantage of making the type's purpose more clear. This seems like a natural development on what the type checker can do.
New description: Some type signatures could be simplified by separating certain elements, either because they are lengthy and can be expressed simpler, to better express intention, or because they are repetitive. A "WhereSignatures" extension would allow for type signatures like the following: {{{#!hs fold :: f -> [a] -> a where f = a -> a -> a -- expresses intention more clearly than: fold :: (a -> a -> a) -> [a] -> a union :: a -> a -> a where a = Map.Map k v -- much shorter/more readable than: union :: Map.Map k v -> Map.Map k v -> Map.Map k v }}} Or maybe even: {{{#!hs fmap :: (a -> b) -> f a -> f b where (Functor f) -- arguably prettier than: fmap :: (Functor f) => (a -> b) -> f a -> f b }}} This minor syntactic sugar is essentially equivalent to local "type" definitions, which provides an advantage of making the type's purpose more clear. This seems like a natural development on what the type checker can do. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
{{{#!hs fold :: f -> [a] -> a where f :: a -> a -> a }}} is certainly confusing, because in the first line `f` is used like a type, but in the second, `f` is used like a value (or `a -> a -> a` is used like a kind
Maybe you meant {{{#!hs fold :: f -> [a] -> a where f = a -> a -> a }}} which could be extended to allow
{{{#!hs fold :: f -> [a] -> a where f :: * f = a -> a -> a }}}
I’m sure the type level programming wizards and dependently typed
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by danso): Replying to [comment:1 nomeata]: programmers will have the greatest need for such an extension, and have a good opinion here. Good catch. I agree that your suggestion makes more sense and have changed the ticket accordingly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): You can today say {{{ fold :: (f ~ a -> a -> a) => f -> [a] -> [a] }}} which does the job reasonably. I doubt it's worth doing more. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:4 simonpj]:
{{{ fold :: (f ~ a -> a -> a) => f -> [a] -> [a] }}}
But doing this changes type inference characteristics, by introducing an equality and making some type variables untouchable. This was pointed out in an earlier bug (sadly, I can't remember any search terms) that highlighted a case where the static semantics of using this sort of trick was different than the expanded form. The place I've wanted a feature like this most is when writing intricate type families. But there, it would be necessary to allow local type family definitions in the `where` clause. All that said, I'm ambivalent about this proposal as stated. It would be useful. But does Simon's trick work often enough? Is it worth specifying, developing, and maintaining this? I'm not sure. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): I don't think it changes the type inference characteristics. Can you give an example? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10794: Extension request: "where" clauses in type signatures -------------------------------------+------------------------------------- Reporter: danso | Owner: Type: feature request | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): No, I don't have one. But I'm sure that there was a ticket complaining about the weirdness of using your trick. However, several minutes of looking through a bunch of tickets has yielded nothing. Maybe I'm imagining things. Until we have evidence of the failure, I agree that we should consider your trick to be a suitable encoding of the proposed idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10794#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC