[GHC] #10756: Allow users to indicate inaccessible patterns
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Consider {{{#!hs {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} data Elem :: * -> * -> * where EZ :: Elem (f , fs) f ES :: Elem fs f -> Elem (f', fs) f elemAbsurd :: Elem () f -> a elemAbsurd _ = error "inaccessible" }}} This catch-all in `elemAbsurd` is very unfortunate, because if I change my datatype and not all cases are inaccessible anymore the type checker will not be warning me. Although of course there is recent work by SPJ et al on inferring more inaccessible cases, I think it would be tremendously useful for users to be able to indicate that patterns are in fact inaccesible. I'd be very happy if I could write {{{#!hs elemAbsurd :: Elem () f -> a elemAbsurd EZ = inaccessible elemAbsurd (ES _) = inaccessible }}} Note that ghc ''can already detect that these patterns are in fact inaccessible'': it won't let me write the above: {{{ T.hs:12:12: Couldn't match type ‘()’ with ‘(f, fs)’ Inaccessible code in a pattern with constructor EZ :: forall f fs. Elem (f, fs) f, in an equation for ‘elemAbsurd’ }}} So I think it should be very very simple to change the type checker to allow to write cases like this if and only if the RHS is a specially designated symbol "inaccessible", which could be defined simply as {{{#!hs inaccessible :: a inaccessible = error "inaccessible" }}} in `GHC.Prim` or something. This would seem like very little work, and a correspondingly tiny patch, but with quite a large payoff. Future work in automatically detecting inaccessible cases would not make existing code using this style wrong, it just means that we have to write fewer inaccessible cases by hand; but even with more sophisticated inference algorithms for inaccessible cases there will still be inaccessible cases remaining. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * cc: george.karachalias@… (added) Comment: I like this idea (although may wish to debate the concrete syntax). But I'd like to hear input from the folks who are implementing the enhanced pattern-exhaustiveness check first. I've cc'd the lead author of that work. Any thoughts, George? When do you expect your patch to land? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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 bgamari): Also, kosmikus has suggested that the syntax proposed above looks a bit too similar to a usual RHS. [https://github.com/idris-lang/Idris-dev/wiki /Unofficial-FAQ#where-is-agdas--pattern-and-what-is-impossible Idris], for instance, has a very clearly different syntax for this, {{{ f : Num a => (n : Nat) -> Vect n a -> Nat f Z [] = 0 f Z (_::_) impossible f (S n) (x::xs) = x + f n xs f (S _) [] impossible }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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 bgamari): == Proposal An `ImpossibleCases` language extension is introduced which turns `impossible` into a keyword when enabled. This keyword can be inserted in the place of a right-hand-side of an equation or case alternative to indicate that the left-hand-side pattern is ill-typed. This is useful for clarifying the meaning of the code to later readers as well as satisfying exhaustiveness warnings when the exhaustiveness check is unable to see that the pattern is ill-typed. To demonstrate this let's consider a standard dependently-typed vector, {{{#!hs data Vect (n::Nat) a where (:::) :: a -> Vect (n-1) a -> Vect n a Nil :: Vect 0 a }}} Perhaps we want a `head` operation on this type (note that this is a toy example; GHC's exhaustiveness checker currently has no trouble identifying the `Nil` case as impossible). An equation would look something like, {{{#!hs head :: (KnownNat (n :: Nat)) => Vect (n+1) a -> a head Nil impossible head (a:::_) = a }}} A case analysis would look like, {{{#!hs head :: (KnownNat (n :: Nat)) => Vect (n+1) a -> a head x = case x of Nil impossible a:::_ -> a }}} This could also be used in `LambdaCase` expressions, {{{#!hs head :: (KnownNat (n :: Nat)) => Vect (n+1) a -> a head = \case Nil impossible a:::_ -> a }}} When the exhaustiveness checker sees a so-marked pattern it will suppress a missing-case warning. == Related Work As noted in the ticket description, the recent (and hopefully soon to be merged) [[http://research.microsoft.com/en-us/um/people/simonpj/papers/pattern- matching/gadtpm.pdf|GADT exhaustiveness]] work will reduce the need for these annotations, however this need will not be eliminated (see the Evaluation section of the paper). Moreover even with perfect exhaustiveness detection these annotations can elucidate complex pattern matches, making it explicit to the reader which cases he needn't worry about. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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): Thanks for writing that up. I like it. My only complaint is the choice of the word `impossible`, which becomes a full-fledged keyword under this proposal. If someone wants to use `ImpossibleCases` and they import a symbol named `impossible`, can they use it? I suppose using it qualified wouldn't conflict. And no exported symbol named `impossible` comes up at http://www.stackage.org/lts-2.22/hoogle?q=impossible I don't have a better suggestion among the set of keywords/keyoperators. So I vote +1 for the proposal exactly as is. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by YitzGale): * cc: gale@… (added) Comment: I propose a modification: that {{{impossible}}} not become a full-fledged keyword, but rather that it only be given special meaning in the context of a pattern expression. I leave as an open question how this should work in a pattern guard. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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): But the only way to bind a variable is in a pattern. That's why it must become a full keyword, in my view. Or have I missed something? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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 YitzGale): Replying to [comment:7 goldfire]:
But the only way to bind a variable is in a pattern. That's why it must become a full keyword, in my view. Or have I missed something?
Sorry, to be more explicit - `impossible` only has special meaning in pattern expressions, and only '''after''' the ''var'' term, which always occurs in first position in pattern expressions that contain it. We can simplify that to say that `impossible` never has special meaning in first position in a pattern expression in any case, since anyway that never makes sense. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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): Are you then suggesting that {{{ -- this is OK: impossible :: Int -- this is OK: impossible = 42 -- this is wrong: Just impossible = Just 42 }}} ? This would indeed bind `impossible` and then it would make sense to use the word in expressions. But I find it strange that the pattern `impossible` works at top-level but not elsewhere... it's just another weird wrinkle in a language that already has too many of them. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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 YitzGale): Replying to [comment:9 goldfire]: Correct. The first two would be valid and retain their current meaning. The third is invalid for two reasons: because `Just` requires an argument, and because the bound RHS value is omitted after an impossible pattern. I'm not sure what you mean by "top level". My proposal is similar to many other features of Haskell as well as almost every other language - that certain tokens are given special meaning in specific syntactic contexts. Why is that a weird wrinkle? A few existing examples: `as` and `qualified` have special meaning only in `import` statements; `forall` and `.` only have special meaning in type expresssions; etc. In general, it's a good idea to keep keywords to a minimum; otherwise the language becomes increasingly awkward to use. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns
-------------------------------------+-------------------------------------
Reporter: edsko | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.10.2
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):
The syntactic construct that assigns values to variables looks like
''pattern'' = ''expression''
What you are proposing is that this becomes
''top_level_pattern'' = ''expression''
where ''top_level_pattern'' is just like ''pattern'', but also admits the
word `impossible`. That is, the thing to the left of an `=` is ''always''
a pattern in Haskell, even if it's a trivially simple one like a bare
identifier.
But I see another way forward here. The problem is that something like
`foo = bar` can be seen in two different lights: `foo` can be a trivial
pattern, or `foo` can be a 0-argument function. Seen as the former, we
have the annoying ''top_level_pattern'' stuff above. Seen as the latter,
this makes more sense. So your proposal would also allow
{{{
impossible x = x + 1
}}}
In that declaration, `impossible` clearly is not in a pattern position, so
it's OK.
Changing the treatment of `foo = bar` from a pattern binding to a function
binding would also fix <
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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 YitzGale): Replying to [comment:11 goldfire]: I agree. I anyway wasn't thinking of turning everything into a pattern binding. Other than type aliases and record syntax, the LHS of = is either a function binding or a pattern binding, both of which include a pattern expression. In both cases `impossible` following the pattern expression makes sense, provided that the pattern expression is non-empty. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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): A binding `foo = bar` is already regarded as a function binding in GHC. From `HsBinds`: {{{ = -- | FunBind is used for both functions @f x = e@ -- and variables @f = \x -> e@ -- -- Reason 1: Special case for type inference: see 'TcBinds.tcMonoBinds'. -- -- Reason 2: Instance decls can only have FunBinds, which is convenient. -- If you change this, you'll need to change e.g. rnMethodBinds -- -- But note that the form @f :: a->a = ...@ -- parses as a pattern binding, just like -- @(f :: a -> a) = ... @ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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: | -------------------------------------+------------------------------------- Changes (by gkaracha): * cc: george.karachalias@… (removed) * cc: gkaracha (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10756: Allow users to indicate inaccessible patterns -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #3483 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * related: => #3483 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10756#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC