Or patterns

[osa1]

Rendered
Trac ticket
/r/haskell thread

[cocreature]

I really like this idea and often wanted to have something like this.

I assume an or-pattern where different parts reference a different set of variables or the variables have different types will just result in an error message?

[osa1]

I assume an or-pattern where different parts reference a different set of variables or the variables have different types will just result in an error message?

That's what I thought, but I think if we do something like:

for pattern in or_pattern:
  type check RHS against pattern

then we can allow different types for same variables in different patterns. Example:

data T a = C1 Int | C2 Bool

f :: T a -> String
f (C1 x | C2 x) = show x

If we type check show x for each pattern and only accept when for all patterns it typechecks I think we can accept this. Then during desugaring we can duplicate right-hand sides to get this:

f a = case a of
        C1 x -> show x
        C2 x -> show x

To keep things simple (and in within the parts of the compiler internals that I understand), I said "same set of variables of same types". We can either generalize this later or right now if type checker experts can chime in here.

One thing to note here is that is we restrict patterns to bind same set of variables of same types I think desugaring gets a lot simpler: we just generate a local function for the RHS, and call it with same set of variables in each case (similar to how fail_ functions generated by the desugarer). It gets more tricky as we generalize because we may have to pass typeclass dictionaries (and maybe some other things that I can't imagine right now).

[mitchellwrosen]

One alternative to this feature is simply a warning for the existence of a wildcard pattern match.

[osa1]

One alternative to this feature is simply a warning for the existence of a wildcard pattern match.

What would be the fix for that warning? Without or patterns you just replace one problem with another (namely, wildcard patterns with repetitive and/or duplicated code).

[mitchellwrosen]

Without or patterns you just replace one problem with another

That's true, but (IMO) it's replacing a big problem (wildcard patterns) with a small(er) one (duplicating the RHS on all the patterns you want to treat uniformly).

[rwbarton]

I would very happy to have these. Ocaml has or-patterns already (https://caml.inria.fr/pub/docs/manual-ocaml/patterns.html#sec108), so we could borrow ideas from its implementation.

A real-world use case where or-patterns would be helpful that I mentioned just the other day to someone working on improving iOS support in GHC:

picCCOpts :: DynFlags -> [String]
picCCOpts dflags
    = case platformOS (targetPlatform dflags) of
      OSDarwin
          -- Apple prefers to do things the other way round.
          -- PIC is on by default.
          -- -mdynamic-no-pic:
          --     Turn off PIC code generation.
          -- -fno-common:
          --     Don't generate "common" symbols - these are unwanted
          --     in dynamic libraries.

       | gopt Opt_PIC dflags -> ["-fno-common", "-U__PIC__", "-D__PIC__"]
       | otherwise           -> ["-mdynamic-no-pic"]
      OSMinGW32 -- no -fPIC for Windows
       | -- ...

The OSiOS case needs to be the same as the OSDarwin case, and an or-pattern (OSDarwin | OSiOS) would be the most direct way to express that. (Otherwise you need to copy the whole OSDarwin case, or refactor the guards and bodies into a new binding and use it in both the OSDarwin and OSiOS cases. If the guards weren't "complete", so that there was a chance that no guard succeeds, then you'd need to duplicate the guards and bodies individually.)

As for syntax, I'm +1 on using | (as opposed to alternatives discussed in the ticket) because it is short, and already a reserved operator. There is a parse conflict with guards (exemplified in the above code snippet) but using parentheses to disambiguate is easy enough.

As for semantics when binding variables of different types, matching on existential constructors, etc., I'd be content with an incremental approach of supporting the simple cases first; that's where most of the value is anyways.

[Ericson2314]

We should have done this along time ago. I use it all the time in Rust too, and miss it all the time in Haskell.

One interesting thing to note is that exhaustive lazy or patterns make sense.

[vagarenko]

Can I use it in case or lambda case:

stringOfT :: T -> Maybe String
stringOfT x = case x of
    T1 s -> Just s
    T2{} | T3{} -> Nothing

like this?

[rwbarton]

Can I use it in case or lambda case:

Yes although in this situation you would need parentheses around T2{} | T3{} (otherwise it parses as a guard).

An or-pattern is again a pattern so it can appear wherever a pattern can, including for example nested within another pattern (Just ('x' | 'y')).

[osa1]

@vagarenko, like @rwbarton said, an or pattern can appear anywhere that a pattern can appear.

OCaml already supports or patterns in full generality (i.e. they can appear anywhere that patterns can appear). This is from Real World OCaml:

let is_ocaml_source s =
  match String.rsplit2 s ~on:'.' with
  | Some (_,("ml"|"mli")) -> true
  | _ -> false

In Rust this is not the case, the reference says "Multiple match patterns may be joined with the | operator.".

---

I started thinking about the implementation. As the first thing I think we may have to make significant changes in the parser. Currently patterns are subsets of expressions, so we have productions like this:

pat     :  exp          {% checkPattern empty $1 }

checkPattern transforms an expression to a pattern:

checkPattern :: SDoc -> LHsExpr RdrName -> P (LPat RdrName)
checkPattern msg e = ...

With this change patterns won't be a subset of expressions, so we may want to first parse for a pattern, and then try to transform it into an expression. Does anyone have any other ideas on this?

[rwbarton]

Pattern syntax was never really a subset of expression syntax (especially before TypeApplications):

Prelude> f @ x

<interactive>:2:1: Pattern syntax in expression context: f@x
Prelude> ~a

<interactive>:3:1: Pattern syntax in expression context: ~a

I'm not sure whether the pattern parser reuses the expression parser out of technical necessity (e.g., we don't know up front whether we are parsing a pattern or an expression) or out of convenience. If it's the latter it might be time to create a separate pattern parser. IIRC the reuse of the expression parser already causes some oddities around the precedence of @ and/or ~.

[goldfirere]

It's out of necessity. If a line begins f x y, the parser doesn't know if it's a naked top-level Template Haskell splice or the beginning of a function definition.

Naked top-level splices are a misfeature, in my opinion.

[saurabhnanda]

Is this proposal to force the pattern-match to match every possible ADT value explicitly? There are times where just having a wildcard _ match is a bug waiting to happen.

Actual use-case -- we start with the following ADT definition and call-sites:

data BookingStatus = Confirmed | Cancelled | Abandoned
computeRemainingSeats :: BookingStatus -> (...)
computeBilling :: BookingStatus -> (...)

Now, assume that within computeAvailability only Confirmed is explicitly matched to result in a reduction of available seats, everything else is matched by _ and results in a no-op. What happens when BookingStatus evolves to have a new value of ManualReview? We want to reduce the number of seats till the manual-review of the booking is complete. However, the compiler will not force us to look at this particular call-site to evaluate this impact.

Another one: assume that within computeBilling only Confirmed is explicitly matched to trigger an invoicing action, others are matched via _ to a no-op. What happens when BookingStatus evolves to have a new value of Refunded, which should trigger a credit-note action? Again, the compiler is not going to help us here.

Therefore, my question. Can we add a pragma to ADTs to disallow wildcards? eg.

data BookingStatus = Confirmed | Cancelled | Abandoned
{-# NoWildCardMatch BookingStatus #-}

Once this is done, having the or pattern will make explicit pattern matches easier to write.

[osa1]

Thanks for the examples @saurabhnanda. Your examples are exactly the same as the second example I gave in the proposal.

About the pragma: it sounds like a good idea, but it's orthogonal to this proposal and can be done separately. Even without or patterns it may be useful, so I suggest creating a new proposal for that.

So no, this is not a proposal to force pattern matching on every possible ADT constructor.

[saurabhnanda]

@osa1 I'm not confident of being able to write all these sections: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposal-submission.rst#content-of-the-proposal-document

[phadej]

I don't really see the value of NoWildCardMatch pragma. Lazy programmer can workaround it by

isConfirmed :: BookingStatus -> Bool
isConfirmed Confirmed = True
isConfirmed Cancelled = False
isConfirmed Abandoned = False

andHereICanBeLazy :: BookingStatus -> IO ()
andHereICanBeLazy bs | isConfirmed = putStrLn "confirmed"
                     | otherwise   = putStrLn "not confirmed"

or in case of non-enums with YourType -> Maybe (Arg1, Arg2) or Prism.

I.e. at the end it will be about discipline in the team, so I don't see
it's good candidate for inclusion into GHC.

OTOH, feel free to experiment with writing hlint rules.
Maybe hlint doesn't support finding wildcard matches, but then experiment with haskell-src-exts,
it shouldn't be too difficult to find wildcard matches and make quick'n'dirty "type inference" (either from type signature, or other pattern match cases).

[peti]

Lazy programmer can workaround it by ...

It wouldn't call a programmer doing that "lazy". It's more like an hostile attacker actively trying to break the rules. Now, it's unfortunate that this issue exists, but it doesn't take away from the usefulness of NoWildCardMatch for those who want to be constructive about writing code that doesn't rely on catch-all default cases.

[simonpj]

I'm not against or-patterns, even mildly in favour.

But

we can allow different types for same variables in different patterns

Let's NOT do this . It would add a huge amount of complexity to a basically-simple feature. Each pattern in an or-group should bind the same term variables, exisitential type variables, and constraints.

Don't forget there is work to do to fix up the pattern-match overlap checker.

[qnikst]

starting from some level of complexity the good complex rule that is catch all but it may be changed in future, and workaround for bypassing the wildcard restriction feature are indistinguishable.
Also example provided by @phadej is completely OK with the NoWildcardMatch, because isConfirmed function uses it.
The only stable way of disallowing wildcard match without introducing bad side effects is to not expose internals but provide deconstructive:

data BookingStatus = Confirmed | NotConfirmed

withBookingStatus onConfirmed onNotConfirmed

Then with the change of the data type - the type of deconstructor will also change and all users will be notified.

[simonmar]

It's out of necessity. If a line begins f x y, the parser doesn't know if it's a naked top-level Template Haskell splice or the beginning of a function definition.

it was a necessity even before top-level naked splices, e.g. in the statements of do or a list comprehension there's a clash between p <- e (a bind) and just e (a guard).

[simonpj]

Shouldn't it be re-opened because of haskell-org/summer-of-haskell#84 (comment) ?

Well, it needs an active champion. Anyone who wants to play that role can of course reopen it.

[LeventErkok]

I'd very much love to see this supported in GHC. It'd make the life of the "working industry programmer" significantly better.

If it helps simplify design/implementation, you can outlaw binding any parameters in the "or" case. I.e., you can pattern-match multiple constructors, so long as no variables are bound in any of those matches. This is a simplification, and I doubt it would take away much from usability in practice, yet deliver a nice solution to practical problems. (Of course, if it doesn't add extra complication, do allow them; but it's an option perhaps for the first version of an implementation?)

[sgraf812]

Yes; perhaps we can deliver on nested (field) matches in a future proposal.

That is, I propose the following change:

-p1 and p2 bind same set of variables.
+p1 and p2 bind no variables, constraints or dictionaries.

In particular, this change entails not having to worry about GADTs and whatnot for now. (No type refinement of the pattern variable is possible either.) I believe that if there is a semantics for or-patterns that can cover GADTs and bound variables, then this semantics can be expressed as a backwards-compatible extension to this simpler semantics.

I think we are rather late to the party:

• OCaml has it
• Rust has it
• Python hast it: https://peps.python.org/pep-0622/#patterns
• Even Java has it (JEP 420 and multiple case labels are possible)
• C# too

Let's ship the MVP that catches 90% and think about the hard 10% case afterwards.

@LeventErkok (or someone who reads this!) would you be up to recycle this proposal into a new one that delivers the MVP?

[nomeata]

When you say

bind no variables, constraints or dictionaries.

Do you mean that the patterns must not bind any of these, or that any bindings are ignored? For variables probably the former (i.e. requiring the programmer to write _ or {}), but for constraints there is no syntax to explicitly not bind them.

Here is an example. Allowed or not?

data T a where
  MkTInt :: T Int
  MkTBool :: T Bool

foo (MkTInt | MkTBool) = ...

[sgraf812]

Do you mean that the patterns must not bind any of these, or that any bindings are ignored?

The latter, at least in Haskell. The former in the desugaring to Core (where it's all just variables, I guess). I should have been more clear. So your foo is allowed, but this bar would be rejected:

data U a where
  MkInt :: U Int
  MkInt2 :: U Int

bar :: U a -> a
bar (MkInt | MkInt2) = 42 :: Int

That is, an or pattern will never provide new Givens such as a ~ Int here.

Perhaps it should just be

-p1 and p2 bind same set of variables.
+p1 and p2 bind no variables.

because the proposal already states, in 1.4.1

The desugaring rule implies that none of the above [Equality constraints, dictionaries, existential types, referred to as "GADTty stuff" below] can be bound by an or pattern.

Maybe that section should be reworded in terms of "Givens"? Not sure that helps. Anyway, my changed proposal would allow GADTs in or patterns (including existentials), but the desugared Core would not bind any of the aforementioned GADTy stuff in the view pattern.

NB: A future proposal could relax this requirement and (semantically) allow more (syntactically valid) programs in the process that would be semantically incorrect in the MVP. I believe that is what the current proposal aimed at and is also what caused it to come to a halt, even after it only tried to focus on simple field binders without GADTy stuff. The details are non-trivial, especially if we want to keep the desugaring to view patterns. Maybe vars where vars is a tuple of the variables bound in the pattern is not enough to carry the Givens or existentials, so why not desugar to a view pattern over Bool.

[nomeata]

Thanks guys clarifying!

[AntC2]

? I think this proposal is in the same design space as the \cases proposal, which is about to land in 9.4. The advantage with \cases is the alts can handle AFAICT per-alt binding different vars; and/or type improvements under a GADT; and different/multiple guards per alt.

As at today, I think you could write a Pattern Synonym/ViewPattern to give a uniform view over diverse constructors -- again with more flexibility of typing. Admittedly that comes at cost of a couple of extra declarations, and some rather clunky code.

[JakobBruenker]

@AntC2 the interaction of Or-patterns with \cases proposals should in principle be exactly the same as the interaction of Or-patterns with function definition equations with multiple patterns, like

f p1 q1 r1 = ...
f p2 q2 r2 = ...

I think in both cases (i.e. here and with \cases) you should be able to replace any of these patterns with an Or-pattern without issues.

[sgraf812]

Note that #522 is an evolution of this proposal that eschews variable bindings altogether (in a forward compatible way), as motivated by #43 (comment). Feel free to offer your opinion there, since this proposal is dead as far as I can tell.

[rhendric]

AFAICT the current state of the world is that #522 was accepted, has an implementation planned to ship with GHC 9.12, and there is not currently another proposal in the works for extending the syntax to include bindings as in this original proposal; is that correct? Or is the next step being discussed somewhere else that I didn't find?

[sgraf812]

Exactly. Or patterns have been merged (https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9229) and will be released with GHC 9.12. There is no active proposal for introducing binders, but feel free to generalise the typing rule in #522.

[rhendric]

feel free to generalise the typing rule in #522.

Early in this very long PR thread, most of the conversation seemed to be in agreement that ‘all inner patterns bind the same variables with the same type’ was a reasonable starting point. So I suppose I would first generalize the current typing rule

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \Gamma_0, \Sigma_i, \Psi_i\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}\ pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \Gamma_0, \Sigma_0, \emptyset\ \large\strut} $$

to

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \Gamma, \Sigma_i, \Psi_i\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}\ pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \Gamma, \Sigma_0, \emptyset\ \large\strut}\ \text{.} $$

Beyond that, I suspect I don't understand the rules of the game. Is this $\Gamma, \Sigma \vdash pat : \tau \leadsto \Gamma, \Sigma, \Psi$ style of pattern type elaborated anywhere? The only references I've found echo your comment here, and while I think I grasp the broad strokes I suspect I'm missing some important details. Have typing rules been specified for, say, constructor patterns and variable patterns, or for case-expressions, using this form of pattern type?

[sgraf812]

The typing rules for pattern types are given on the very last page of https://mpickering.github.io/pattern-synonyms-extended.pdf.

Yes, ‘all inner patterns bind the same variables with the same type’ sounds reasonable, and it should also be possible to specify the declarative typing rule along the lines of what you did.

The one you presented almost works. Such a specification is a good first step towards an algorithmic implementation, however note that Ψi lists existential type variables unleashed by GADT constructors for example, and Γ might contain match variables in the type of which those existentials occur. Since your rule cleverly restricts all alternatives to the same Γ, this forces subsets of Ψi to equate. But since these binders in Γ reference a subset of Ψi in their type, your rule may no longer return the empty set as existentials in scope after the match, otherwise you lose well-scopedness.

In the implementation, you would most likely need to unify any introduced existentials and binders in Γ and keep them in scope, while dropping the rest of ψi and Σi.
However, I'm unsure whether the current implementation mechanism (which works similar to lazy patterns ~Refl which also do not introduce existentials or evidence) can be adapted. It is likely you would need to implement these steps yourself, as there is no prior work.

Thus, it might be simpler to restrict

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \Gamma, \Sigma_i, \Psi_i \quad \Psi_i \text{ not free in } \Gamma\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}\ pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \Gamma, \Sigma_0, \emptyset\ \large\strut}\ \text{.} $$

At the end of the day, the restricted form of the proposal was just to color the bike shed and ship something. Perhaps this form is doable as well.

[rhendric]

Ah, lovely! I didn't realize the pattern synonyms paper had this tucked away in the appendix. Thank you for the pointer.

I had assumed that $\Psi_i$ contained renamed variables, such that they could not be shared between inner patterns and therefore could not appear in $\Gamma$. If that's not the case, I'm concerned that the existing typing rules, ignoring or-patterns entirely, are unsound. Consider:

data T where
  C :: forall a. Eq a => a -> T

badEq :: (T, T) -> Bool
badEq (C x, C y) = x == y

Desugaring badEq to:

badEq = \a -> case a of (C x, C y) -> x == y

and applying the typing rules from the paper (large SVG image, sorry, I haven't figured out a good way to render these derivations):

we can see that there is a valid derivation for this program per the rules, but clearly badEq (C 1, C True) would lead to ruin. The rules only work if the same $\beta$ isn't used in both branches of the proof for (C x, C y), which means that the $\beta$ introduced into $\Psi$ ought to be a fresh name substituted into the relevant types (the substitutions in the rules only cover universally-quantified variables, not existentially-quantified ones).

With that change, there would be no need for ‘$\Psi_i$ not free in $\Gamma$’.

While I'm picking nits, having now spent some time staring at the rules, I think the intent is that the contexts on the right of the judgment do not contain the contexts on the left of the judgment as subsets, but instead represent only extensions (the base rules for variable patterns and wildcards use empty sets on the right of the judgment, for example). So the rule currently implemented should probably be written as

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \emptyset, \Sigma_i, \Psi_i\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \emptyset, \emptyset, \emptyset\ \large\strut}\ \text{,} $$

and my conservative extension as

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \Gamma, \Sigma_i, \Psi_i\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \Gamma, \emptyset, \emptyset\ \large\strut}\ \text{.} $$

But now that I have enough context to be dangerous I have a notion of a more liberal rule I could propose as a further step. Still proving to myself that it's sound under some appropriate reinterpretation of the rules in the paper, though.

[sgraf812]

The rules only work if the same isn't used in both branches of the proof for (C x, C y)

I think your example highlights an important point: In the product rule ($K\ pat_1\ ...\ pat_n$), all the $\Psi_i$ must be distinct (because every existential gets instantiated to a binding site of a fresh ty var). But in the sum rule (or patterns), I don't think we need this same restriction! For example, the following program could reasonably be accepted:

data T where
  C1 :: forall a. a -> (a -> Int) -> T
  C2 :: forall a. a -> (a -> Int) -> T

foo :: T -> Int
foo (C1 x f; C2 x f) = f x

But of course, we could only ever accept such a program if those $\Psi_i$ allowed overlap.
Since it is certainly possible and not prohibited by binding structure to type such a program, I would rather have an explicit condition saying "(all $\Psi_i$ distinct)" instead of having the user playing a guessing game.

While I'm picking nits, having now spent some time staring at the rules, I think the intent is that the contexts on the right of the judgment do not contain the contexts on the left of the judgment as subsets, but instead represent only extensions

Indeed, that's a good point, and easy to fix as well as you point out.

With that change, there would be no need for ‘ not free in ’.

I think so as well. But it's better to be clear and give that condition in one form or another. I think "(all $\Psi_i$ distinct)" is clearer than the freeness constraint.

But now that I have enough context to be dangerous I have a notion of a more liberal rule I could propose as a further step.

That's great news :) I'll be happy to assist with the implementation, although perhaps I'm not the best resource.

[rhendric]

Okay, here's my current thinking about the theory before shifting gears to implementation. First, I propose some modifications to the typing rules as they appear in the appendix, half to resolve soundness issues, half to cover a few more programs that GHC currently admits. I hope nobody is sick of my underinformed pedantry yet.

Constructor patterns

Soundness issue: renaming $\overline\beta$

As previously discussed, the reuse of $\overline\beta$ between inner patterns causes a soundness issue. Simply stating ‘$\Psi_i$ all disjoint’ is not, pedantically speaking, sufficient, because the $\overline\beta$ are determined by the declaration of $K$, so we are not free to choose fresh $\overline\beta$ as we wish. So we should also, in this rule, instantiate fresh $\overline\beta'$ names and substitute them wherever $\Theta$ and $\overline\tau$ are used.

Coverage issue: left-to-right scoping

GHC, in its wisdom, admits functions such as this:

data T a where
  C1 :: forall a b. Show b => (T a -> T b) -> T a
  C2 :: a -> T a

f :: (T a, T a) -> String
f (C1 g, g -> C2 x) = show x

This demonstrates that term variables (g), existential types (b as instantiated by C1 g), and constraints (Show b) are all propagated across constructor patterns from left to right. The existing rule does not reflect this, but it's an easy fix—extend the contexts for each inner pattern with the extensions produced by all the previous ones.

This might seem like a mere vanity correction, but there is an ulterior motive: sequencing the contexts between inner patterns removes the need for an explicit premise that the $\Psi_i$ be disjoint. Each inner pattern must only add variables to $\Psi_i$ that don't appear in its input contexts, and will chain its output contexts into the next pattern, so the only way that a variable in $\Psi_i$ can be shared by two $\Psi_i$ is if its earlier appearance occurs nowhere in input or output contexts—quite a harmless thing!

Taken together, the revised constructor pattern rule is

$$ \cfrac{ \begin{array}{c} K : \forall\overline\alpha\overline\beta.\Theta \Rightarrow \tau_1\to\ldots\to\tau_n \to T\,\overline\alpha \\\ (\Gamma_0,\ldots,\Gamma_{i - 1}),\left(\Sigma_0,\ldots,\Sigma_{i - 1},\Theta\left[\overline\tau'/\overline\alpha,\overline\beta'/\overline\beta\right]\right) \vdash \mathit{pat}_i : \tau_i\left[\overline\tau'/\overline\alpha,\overline\beta'/\overline\beta\right] \leadsto \Gamma_i, \Sigma_i, \Psi_i \\\ \mathit{FV}(\Gamma_0, \Sigma_0) \cap \overline\beta' = \emptyset \end{array} } {\Gamma_0, \Sigma_0 \vdash K\,\mathit{pat}_1 \ldots \mathit{pat}_n : T\,\overline\tau' \leadsto \overline\Gamma, \left(\overline\Sigma,\Theta\left[\overline\tau'/\overline\alpha, \overline\beta'/\overline\beta\right]\right), \left(\overline\Psi, \overline\beta'\right)} $$

Pattern synonyms

Both of the constructor pattern issues translate to pattern synonyms mutatis mutandis, so I will simply present the revised rule.

$$ \cfrac{ \begin{array}{c} P : \forall\overline\alpha.\Theta_\text{req} \Rightarrow \forall\overline\beta.\Theta_\text{prov} \Rightarrow \tau_1\to\ldots\to\tau_n \to T\,\overline\alpha \quad \Sigma_0 \vdash \Theta_\text{req}\left[\overline\tau'/\overline\alpha,\overline\beta'/\overline\beta\right] \\\ (\Gamma_0,\ldots,\Gamma_{i - 1}),\left(\Sigma_0,\ldots,\Sigma_{i - 1},\Theta_\text{prov}\left[\overline\tau'/\overline\alpha,\overline\beta'/\overline\beta\right]\right) \vdash \mathit{pat}_i : \tau_i\left[\overline\tau'/\overline\alpha,\overline\beta'/\overline\beta\right] \leadsto \Gamma_i, \Sigma_i, \Psi_i \\\ \mathit{FV}(\Gamma_0, \Sigma_0) \cap \overline\beta' = \emptyset \end{array} } {\Gamma_0, \Sigma_0 \vdash P\,\mathit{pat}_1 \ldots \mathit{pat}_n : T\,\overline\tau' \leadsto \overline\Gamma, \left(\overline\Sigma,\Theta_\text{prov}\left[\overline\tau'/\overline\alpha, \overline\beta'/\overline\beta\right]\right), \left(\overline\Psi, \overline\beta'\right)} $$

Let-expressions

I have also found some issues with the let-expression rule and will share them if they become relevant; this comment is too long already.

---

Or-patterns

Having completed my revision of the original typing rules, here are three editions of the rule for or-patterns: Free, Professional, and Ultimate (the first two are simply recaps).

Free (of bindings)

What is currently implemented:

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \emptyset, \Sigma_i, \Psi_i\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \emptyset, \emptyset, \emptyset\ \large\strut} $$

Professional (all that most working Haskellers should need, but nothing fun)

What I previously proposed:

$$ \cfrac{\Gamma_0, \Sigma_0 \vdash pat_i : \tau \leadsto \Gamma, \Sigma_i, \Psi_i\Large\strut} {\ \Gamma_0, \Sigma_0 \vdash \texttt{(}pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n \texttt{)} : \tau \leadsto \Gamma, \emptyset, \emptyset\ \large\strut} $$

Ultimate

Should be sound but may raise some eyebrows—admits everything I can imagine soundly admitting:

$$ \cfrac { \begin{array}{c} \Gamma_0, \Sigma_0 \vdash pat_i : \tau_0 \leadsto \Gamma_i, \Sigma_i, \Psi_i \quad \Gamma_i, (\Sigma_0, \Sigma_i) \vdash x_j : \tau_j\left[\overline{\tau_i}'/\overline\beta\right] \quad (\Sigma_0, \Sigma_i) \vdash \Theta\left[\overline{\tau_i}'/\overline\beta\right] \\\ \mathit{FV}(\Gamma_0, \Sigma_0) \cap \overline\beta = \emptyset \quad \mathit{FV}(\overline\tau, \Theta) \cap \overline\Psi \subseteq \overline\beta \end{array} } {\Gamma_0, \Sigma_0 \vdash \texttt{(}pat_1\texttt{;}\ \ldots\texttt{;}\ pat_n\texttt{)} : \tau_0 \leadsto \overline{x : \tau}, \Theta, \overline\beta} $$

Note that there is some complex indexing going on here: $i$ ranges over the alternatives in the or-pattern, while $j$ ranges over the term variables bound by each inner pattern (and thus by the or-pattern itself). Additionally, while $\tau_j$ is a type corresponding to the bound term variable $x_j$, $\overline{\tau_i}'$ is a vector of types used by $\mathit{pat}_i$ as substitutions for the vector of type variables $\overline\beta$.

Some properties you might want out of an or-pattern typing rule, and how the Ultimate edition satisfies them:

Idempotency

In the (p; ...; p) case (including $n = 1$!), this rule should admit exactly the things that would be admitted when using the inner pattern directly. To see that it admits at least those things, set $\overline\beta = \overline{\tau_i}' = \Psi_1$, $\overline{x : \tau} = \Gamma_1$, $\Theta = \Sigma_1$, and constrain the $\Gamma_i$, $\Sigma_i$, and $\Psi_i$ to be equal if $n > 1$. I don't yet have a proof that it admits only those things, though I think the desugaring argument below suggests this.

Desugaring

If a typing of an or-pattern is admitted by this rule, then we can produce an admissible typing of an equivalent view pattern, similar to the desugaring suggested in the OP's proposal text. The one difference: to capture existentials and constraints, a single-constructor data type K is postulated for the specific desugaring, in place of the tuple type used by the OP's proposal. The data type has no properties that differentiate it from one that would be defined by hand; it is not treated specially.

Part 1:

Part 2:

With $\overline\alpha'$ defined to be $\mathit{FV}(\text{output contexts}) - \overline\beta'$, all of the premises in blue can be derived from the premises of the or-pattern rule. The postulated constructor K appears in brown.

---

Now for the practical concerns.

There will be some who object that programs like this, without anything existential, visibly constrained, or GADT-like, should not be accepted:

data NotFancy = C1 Int Int | C2 Char Char

less :: NotFancy -> Bool
less (C1 x y; C2 x y) = x < y

They might be right, but I don't mind this at all. It's only confusing if you think about it hard enough to wonder what the type of x and y is, but not hard enough to arrive at the only possible conclusion in a language without intersection types.

Still, maybe we should consider gating the difference between Professional and Ultimate behind a GHC extension, so as not to cause anyone in that middle band to run away screaming.

From the perspective of an implementation, there seems to be a dismaying amount of unknown variables floating around in the Ultimate rule. I'm not qualified to speak to how difficult this is to do, but I imagine the unknowns to be resolved with something like the following algorithm:

1. First determine the cardinality of $\overline{x : \tau}$. Check the inner patterns, collect their bindings, and ensure that they bind the same variable names.
2. For each $j$, if all bindings of $x_j$ have the same concrete type, assign that to $\tau_j$. If not, instantiate a meta variable for $\tau_j$.
3. There's a CPS transform in the pattern-compiling logic, I would guess? Each pattern receives a success continuation and a failure continuation, or something? Assuming so, run type inference on the success continuation, using the types assigned in step 2. Generalize any remaining unknown metas as the $\overline\beta$ set. Assign any unsolved constraints to $\Theta$.
4. Assuming a nonempty $\overline\beta$, to determine the $\overline{\tau_i}'$, for each inner pattern, check that the success continuation can be called with $\overline x$ as bound in $\Gamma_i$, given $\Sigma_i$ and the outer environment. Since the success continuation has been type-checked, this doesn't mean reanalyzing the whole continuation term—only its type. The inferred type arguments to the continuation are the $\overline{\tau_i}'$, and at this point we are done (or we have found a type error somewhere and have failed).

I look forward to being told how my guesses-in-the-dark at how GHC works are incompatible with reality.

I'll be happy to assist with the implementation, although perhaps I'm not the best resource.

The last time I tried to implement a feature of even basic-level complexity in GHC I got lost in the weeds after a week and gave up; I'll take any help I can get! Having https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9229 in place as a starting point should give me an advantage over last time. Though it looks like I may have to finally learn what the heck a ‘zonk’ is.

[rhendric]

Implementation question for @sgraf812 or anyone else:

How should the renamer rename variables bound by or-patterns? Should \(x;x) -> x be renamed to:

• \(x_0; x_0) -> x_0 — conceptually it's all the same name, but now names can be bound multiple times
• \(x_0; x_1) -> x_1 — principle shminciple, this is the easy way and the typechecker and desugarer can fix up names as needed
• \(x_0; x_1)[hidden data: this pattern binds x_2 from {x_0, x_1}] -> x_2 — most accurate, but requires extending the pattern type, and now maybe dumping patterns like this becomes awkward or difficult to interpret

I figure unused name warnings are going to be relevant to this decision but I haven't gotten there yet, and I don't know in what direction they'd influence things.

[simonpj]

Before investing too much in an implementation, would it be possible to have a specification, in the form of a GHC proposal?

I vaguely remember issues to do with existentials...

[rhendric]

If you want one strongly, then yes, but I'd consider myself still exploring whether I'm a good person to bring a proposal and how liberal that proposal would be. Is it not typical to hack out a prototype implementation prior to bringing a formal proposal?

It would not be substantially different from this proposal except possibly accepting more of the examples, depending on which typing rule we use out of the two possibilities here. One of those should accommodate the existential issues, as far as I understand them, at the level of theory. Whether it's at all practical to implement is the question I'm currently pursuing.

[simonpj]

Indeed, it's absolutely fine to explore implementations. I'm just wanting to avoid a hard working contributor investing lots of effort in an implementation, only to find that the Steering Committee doesn't like the proposal, or finds serious flaws, or suggests alternatives. But nothing stops you exploring, provided you are content that subsequent debate might change the design you are implementing.

[AntC2]

I'm confused. From this #43 was spun-off #522, which was accepted and with some later mods. So is the continuing discussion here building on that spin-off or somehow orthogonal to it?

wrt the implementation for whatever you're exploring here, wouldn't it be easier to build a PatternSynonym that's equivalent, then take its semantics?

[rhendric]

I necro'd this thread with this comment asking if a continuation was being discussed anywhere else; it seemed not. #522 was a reduction in scope of #43, so I figured this was the most likely spot to discuss returning to the scope of #43 or something like it.

I don't think involving patsyns would make anything simpler; you'd need a view pattern to implement a patsyn for this and in that case you might as well use the view pattern directly, as #43 proposed.

[sgraf812]

In reply to #43 (comment):

The existing rule does not reflect this [left-to-right scoping], but it's an easy fix

Agreed. I wonder what is the best place to commit up-to-date typing rules to. I think Artin Ghasivand is currently working with Simon on setting down typing rules for GHC Haskell. He might be interested.

At any rate it is indeed hard to review if old and new rule are not written side-by-side, but I agree 100% with your written assessment on Constructor patterns.

Ultimate rule

Note that a premise in an inference rule is satisfied if it is true for some instantiation of its free variables. This is already a bit shady for index $i$, where I'm actually missing an overbar in the $pat_i$ premise; otherwise the rule says "it's enough for at least one of the $pat_i$ to satisfy this premise". (An overbar means "for all syntactic (thus finite) instances of $i$", see Computer Science Metanotation.) Arguably since $pat_i$ also occurs in the goal, it is actually clear from context that we must have similar derivations for each of the $pat_i$.

However, since $j$ only occurs in one of the premises, it is enough to find one $j$ for which you can type $x_j$. I think you want a double overbar here, one for $i$ and one for $j$, so that your rule says that $x_j$ must be typeable for every $i$.

(I read past the desugaring into a data constructor $K$ at this point, but I believe it's theoretically feasible as well.)

less (C1 x y; C2 x y) = x < y

I'm a bit confused by how your Ultimate rule would allow to type such a thing. Specifically, I fail to see how $\Sigma_i$ contains the necessary Ord constraints to imply $\Theta$. Besides, it kind of gets me running away screaming as well.

---

I would suggest to propose the "Professional" rule first to gather feedback and experience while implementing it.
We can always relax to some form of "Ultimate" later, but going with "Ultimate" straight away bears the potential to get hung up on discussing and implementing features for the ~1% use case it enables.

[s-and-witch]

How should the renamer rename variables bound by or-patterns?

I recommend you to take a reference from how pattern signatures are implemented, because they solve almost the same problem. Consider this example:

f (_ :: (a, a)) = ()

Here, the first a is a binding, while the second one is a usage. However, pattern signatures don't exactly match scoping of or-patterns. Both a are usages in the next example:

f :: forall a. ...
f (_ :: (a, a)) = ()

Pattern signatures store all the type variables that they bring into scope in extension field, so the answer would be

\(x_0; x_0)[hidden data: this or-pattern brings x_0 into scope] -> x_0

[AntC2]

you'd need a view pattern to implement a patsyn

Ah, very true. And ViewPatterns are an anti-feature. I find when reasoning about patterns that Simon's suggestion/notation helps me see the wood for the trees. To take the Or-like example 2 from here, I write:

pattern DString :: String -> D -- get the String within D, if possible
pattern DString s <- d | s <- case d of
                                  (D1 s_1 _) -> s_1
                                  (D2 s_2 _) -> s_2

So to answer your q, there are three variables, none of which should get unused warnings.

As to how the code appears, I fear your "principle shminciple" isn't going to fly. Consider

data D = D4 Int Int Bool | D5 Bool Int Int

\(D4 i_0 i_1 b_2; D5 b_3 i_4 i_5) -> D4 (i_1@i_4) (i_0@i_5) (b_2@b_3)    -- permute the Ints

I've used an @s-pattern. (Noting the usage might be in an arbitrarily complex data structure.) Currently @ on RHS is illegal syntax, but possible confusion with TypeApplications.

---

What's with that guard on RHS? Consider example 1 from that proposal:

newtype ZipList a = ZipList [a] 

pattern ZCons :: a -> ZipList a -> ZipList a
pattern ZCons x (ZipList xs) = ZipList ( x : xs )               -- the underneath/builder equation
                                                                -- but we can't have a constructor in the LHS pattern
pattern ZCons x zxs | (ZipList xs) <- zxs = ZipList ( x : xs )  -- but now variables are unbalanced/can't be bidir
pattern ZCons x zxs | (ZipList xs) <- zxs = ZipList ( x : xs ) | zxs <- (ZipList xs)

In the builder direction, use the guards on LHS, ignore those on RHS; in the matcher vv. Then we have each side of the = nicely balanced, with each being a pattern.

pattern Succ x | x1 <- x + 1 = x1 | x <- x1 - 1

[rhendric]

@sgraf812

Note that a premise in an inference rule is satisfied if it is true for some instantiation of its free variables.

I inferred inductively, and perhaps foolishly, from the source paper that indexes were treated not as free variables in this sense but as something to be quantified over for each judgment, with overbars used for intra-judgment sequences. I was trying to match that convention; if the result is confusing, I'd probably choose to prefix $\bigwedge_i,\bigwedge_j$ to the relevant judgments instead of nesting overbars. (That $x_j : \tau_j\left[\overline\tau_i'/\overline\beta\right]$ subexpression is nasty to get right if overbars are used to bind indexes; there are three dimensions being quantified over here, two at the level of the judgment and one within the substitution, so I'd have something like $\overline{\overline{\ldots x_j : \tau_j\left[\overline{\tau'_{i,k}/\beta_k}^k\right]\ldots}^j}^i$ going on... yikes!)

I'm a bit confused by how your Ultimate rule would allow to type such a thing. Specifically, I fail to see how $\Sigma_i$ contains the necessary Ord constraints to imply $\Theta$.

The $\Sigma_i$ don't; $\Sigma_0$ does (assuming a standard Prelude). For this example, we have

$$ \begin{align} \tau_1 &= \beta_1 \\\ \tau_2 &= \beta_1 \\\ \Theta &= \mathit{Ord}\;\beta_1 \\\ \tau'_{1,1} &= \mathit{Int} \\\ \tau'_{2,1} &= \mathit{Char} \\\ \Gamma_1 &= \{x : \mathit{Int}, y : \mathit{Int}\} \\\ \Gamma_2 &= \{x : \mathit{Char}, y : \mathit{Char}\} \\\ \Sigma_1, \Sigma_2, \Psi_1, \Psi_2 &= \emptyset \end{align} $$

so satisfying the premises $(\Sigma_0, \Sigma_i) \vdash \Theta\left[\overline\tau'_i/\overline\beta\right]$ requires $\Sigma_0 \vdash \mathit{Ord}\;\mathit{Int}$ for $i = 1$ and $\Sigma_0 \vdash \mathit{Ord}\;\mathit{Char}$ for $i = 2$.

It's just like a polymorphic function: the RHS is generalized over types and constraints, and each alternative of the or-pattern, like a call to a polymorphic function, is responsible for providing type arguments and satisfying any constraints with those type arguments substituted in. But unlike with polymorphic functions, the site of the or-pattern is adjacent to the term being generalized, without an intermediate function term that needs a type from the user's perspective. Many of the objections to generalization don't seem to apply when the thing-to-be-generalized is defined with a new syntax that signals that generalization is intended to happen.

I would suggest to propose the "Professional" rule first to gather feedback and experience while implementing it. We can always relax to some form of "Ultimate" later, but going with "Ultimate" straight away bears the potential to get hung up on discussing and implementing features for the ~1% use case it enables.

Oh, I'm definitely starting with Professional! But if that ends up being within my grasp I think an implementation of Ultimate would be informative enough to be worth trying, and subsequently discussing. I'd expect a lot of the uncertainty around a more powerful rule to stem from questions like how much complexity would it add to the implementation and would it make error messages worse, and if those questions can be answered then we'd all be in a better position to compare the different rules on their merits and not on the amount of uncertainty around them.

@s-and-witch

I recommend you to take a reference from how pattern signatures are implemented, because they solve almost the same problem.

Very useful insight; thank you!

[subterfugue]

@rhendric Awesome work! I've also been wanting for some bindings in Haskell's or patterns. It feels like a peculiar limitation, but I appreciate it since it got us orpats so quickly. What's your progress on it, if you don't mind?

[rhendric]

@subterfuge, I did manage to fumble together an implementation that works on the basics, but I stalled out at making a formal proposal based on it. I'd be happy to work with someone else on moving this forward, or I might get back around to doing it myself when the spirit moves me.

[subterfugue]

@rhendric i'm not too knowledgeable about it, but i can probably learn! just let me know if you've got anything that needs help. i'm a little interested in playing with the impl if you don't mind!