Elimination rules.

When type theorists consider a programming language, we break it down like this:
	•	What are the kinds of fundamental and derived types in the language?
	•	For each type, what are its introduction rules, i.e. how do you get values of that type?
	•	For each type, what are its elimination rules, i.e. how do you use values of that type?

Swift has a pretty small set of types right now:
	•	Fundamental types:  currently i1, i8, i16, i32, and i64; eventually float and double; maybe others.
	•	Functions.
	•	Tuples.  Heterogenous fixed-length aggregates.   Swift's system provides two basic kinds: positional and labelled.
	•	Arrays.  Homogenous fixed-length aggregates.
	•	Algebraic data types (ADTs), introduce by oneof.  Closed disjoint unions of heterogenous fixed-length aggregates.
Adding generics won't affect this, because "unapplied" generic types aren't first-class, and "applied" generic types are always one of the above (probably always ADTs, but it doesn't matter here).  But adding any other kind of type (vectors seem likely) means we need to consider its intro/elim rules.

For most of these, intro rules are just a question of picking syntax, and we don't really need a document for that.  So let's talk elimination.  Generally, an elimination rule is a way at getting back to the information the intro rule(s) wrote into the value.  So what are the specific elimination rules for these types?  How do we use them, other than in type-generic ways like passing them as arguments to calls?

Functions are used by calling them.  This is something of a special case:  some values of function type may carry data, there isn't really a useful model for directly accessing it.  Values of function type are basically completely opaque.
Scalars are used by feeding them to primitive binary operators.  This is also something of a special case, because there's no useful way in which scalars can be decomposed into separate values.
Tuples are used by projecting out their elements.
Arrays are used by projecting out slices and elements.
ADTs are used by projecting out elements of the current alternative, but how we determine the current alternative?

Alternatives for alternatives.

I know of three basic designs for determining the current alternative of an ADT:
	•	Visitor pattern:  there's some way of declaring a method on the full ADT and then implementing it for each individual alternative.  You do this in OO languages mostly because there's no direct language support for closed disjoint unions (as opposed to open disjoint unions, which is essentially just subclassing).
	⁃	plus: doesn't require language support
	⁃	plus: easy to "overload" and provide different kinds of pattern matching on the same type
	⁃	plus: straightforward to add interesting ADT-specific logic, like matching a CallExpr instead of each of its N syntactic forms
	⁃	plus: simple form of exhaustiveness checking
	⁃	minus: cases are separate functions, so data and control flow is awkward
	⁃	minus: lots of boilerplate to enable
	⁃	minus: lots of boilerplate to use
	⁃	minus: nested pattern matching is awful
	•	Query functions:  dynamic_cast, dyn_cast, isa, instanceof
	⁃	plus: easy to order and mix with other custom conditions
	⁃	plus: low syntactic overhead for testing the alternative if you don't need to actually decompose
	⁃	minus: higher syntactic overhead for decomposition
	⁃	isa/instanceof pattern requires either a separate cast or unsafe operations later
	⁃	dyn_cast pattern needs a fresh variable declaration, which is very awkward in complex conditions
	⁃	minus: exhaustiveness checking is basically out the window
	⁃	minus: some amount of boilerplate to enable
	•	Pattern matching
	⁃	plus: no boilerplate to enable
	⁃	plus: hugely reduced syntax to use if you want a full decomposition
	⁃	plus: compiler-supported exhaustiveness checking
	⁃	plus: nested matching is natural
	⁃	plus: with pattern guards, natural mixing of custom conditions
	⁃	minus: syntactic overkill to just test for a specific alternative (e.g. to filter it out)
	⁃	minus: needs boilerplate to project out a common member across multiple/all alternatives
	⁃	minus: awkward to group alternatives (fallthrough is a simple option but has issues)
	⁃	minus: traditionally completely autogenerated by compiler and thus not very flexible
	⁃	minus: usually a new grammar production that's very ambiguous with the expression grammar
	⁃	minus: somewhat fragile against adding extra data to an alternative

I feel that this strongly points towards using pattern matching as the basic way of consuming ADTs, maybe with special dispensations for querying the alternative and projecting out common members.  I'll ignore that 

Pattern matching was probably a foregone conclusion, but I wanted to spell out that having ADTs in the language is what really forces our hand because the alternatives are so bad.  Once we need pattern-matching, it makes sense to provide patterns for the other kinds of types as well.

Selection statement.

This is the main way we expect users to employ non-obvious pattern-matching.  We obviously need something with statement children, so this has to be a statement.  That's also fine because this kind of full pattern match is very syntactically heavyweight, and nobody would want to embed it in the middle of an expression.  We also want a low-weight matching expression, though, for relatively simple ADTs.

  statement ::= 'match' expr '{' case-group-list '}'
  case-group-list ::= case-group
  case-group-list ::= case-group case-group-list
  case-group ::= case-pattern+ stmt-brace-item+
  case-pattern ::= 'case' expr ':'
  case-pattern ::= 'pattern' pattern pattern-guard? ':'
  pattern-guard ::= 'where' expr

We're intentionally not using "switch" here because the syntax is too similar to C but the semantics are a bit different.  This is a bit subtle, but honestly there should be enough other clues.  The keywords here are all up for debate.

Despite the lack of grouping braces, the semantics are that the statements in each case-group form their own scope, and falling off the end causes control to resume at the end of the match statement — i.e. "implicit break", not "implicit fallthrough".  Chris seems motivated to eventually add an explicit 'fallthrough' statement.  If we did this, my preference would be to generalize it by allowing the match to be reperformed with a new value.  But I also think having local functions removes a lot of the impetus.

Syntactically, braces and the choice of case/pattern keywords are all bound together.  The thinking goes as follows.  In Swift, statement scopes are always grouped by braces.  It's natural to group the cases with braces as well.  Doing both lets us avoid a 'case' keyword, but otherwise it leads to ugly style, because either the last case ends in two braces on the same line or cases have to further indented.  Okay, it's easy enough to not require braces on the match, with the grammar saying that cases are just greedily consumed — there's no ambiguity here because the match statement is necessarily within braces.  But that leaves the code without a definitive end to the cases, and the closing braces end up causing a lot of unnecessary vertical whitespace, like so:
  match (x)
  case :foo {
    …
  }
  case :bar {
    …
  }
So instead, let's require the match statement to have braces, and we'll allow the cases to be written without them:
  match (x) {
  case :foo:
    …
  case :bar:
    …
  }
That's really a lot prettier, except it breaks the rule about always grouping scopes with braces (we *definitely* want different cases to establish different scopes).  Something has to give, though.

Also, ":foo:" is pretty unfortunate.  We want to separate the case from its body — it's a huge cue — and as mentioned we'd prefer to do it without requiring open/close punctuation.  Colon seems obvious, since there's precedent in C and it's even roughly the right grammatical function;  it just looks a little silly after ":name".

The semantics of a match-statement are to first evaluate the value operand, then proceed down the list of case-patterns and execute the statements for the first case-pattern that is satisfied by the value.  It is an error if a case-pattern can never trigger because the earlier case-patterns are exhaustive.

A 'case' is satisfied if the value satisfies the evaluated case operand.  The basic behavior will be an equality test, but there will be some point of extension to allow library "patterns" like "4..8".  The case operand does not need to be a "constant expression" — the expression can even have side-effects, although that's obviously poor style.   A 'case' never binds variables.

A 'pattern' is satisfied if the pattern is satisfied and the pattern-guard expression (if present) evaluates to true.  The pattern-guard result must be usable as a logic operand.  The guard expression is not evaluated if the pattern is not fully satisfied.  Variables in the pattern are bound before the guard is evaluated.

All of the case-patterns in a case-group must bind exactly the same variables with exactly the same types.

Since falling out of the match is not unreasonable, there's a colorable argument that non-exhaustive matches should be okay, but I'm inclined to say that they should be errors and people who want non-exhaustive matches can put in catch-all patterns.  The only complication with checking exhaustiveness is pattern guards.  The obvious conservatively-safe rule is to say "ignore guarded cases during exhaustiveness checking", but some people really want to write "where x < 10" and "where x >= 10", and I can see their point.  At the same time, we really don't want to go down that road.

Patterns come up (or potentially come up) in a few other places in the grammar:

Var bindings.

Variable bindings only have a single pattern, which has to be exhaustive, which also means there's no point in supporting guards here.  I think we just get this:
  decl-var ::= 'var' attribute-list? pattern value-specifier

Function parameters.

The functional languages all permit you to directly pattern-match in the function declaration, like this example from SML:
  fun length nil = 0
    | length (a::b) = 1 + length b

This is really convenient, but there's probably no reasonable analogue in Swift.  One specific reason:  we want functions to be callable with keyword arguments, but if you don't give all the parameters their own names, that won't work.

The current Swift approximation is:
  func length(list : List) : Int {
    match list {
    pattern :nil: return 0
    pattern :cons(_,tail): return 1 + length(tail)
    }
  }

That's quite a bit more syntax, but it's mostly the extra braces from the function body.  We could remove those with something like this:
  func length(list : List) : Int = match list {
    pattern :nil: return 0
    pattern :cons(_,tail): return 1 + length(tail)
  }
Anyway, that's easy to add later if we see the need.

Assignment.

This is a bit iffy.  It's a lot like var bindings, but it doesn't have a keyword, so it's really kindof ambiguous given the pattern grammar.

Also, l-value patterns are weird.  I can come up with semantics for this, but I don't know what the neighbors will think:
  var perimeter : double
  :feet(x) += yard.dimensions.height  // returns Feet, which has one constructor, :feet.
  :feet(x) += yard.dimensions.width

It's probably better to just have l-value tuple expressions and not work in arbitrary patterns.

Pattern-match expression.

This is an attempt to provide that dispensation for query functions we were talking about.

I think this should bind looser than any binary operators except assignments;  effectively we should have
  expr-binary ::= # most of the current expr grammar

  expr ::= expr-binary
  expr ::= expr-binary 'matches' pattern pattern-guard?

The semantics are that this evaluates to true if the pattern and pattern-guard are satisfied.  If the pattern binds variables, it's an error if the expression isn't immediately used as a condition;  otherwise, the variables are in scope in any code dominated by the 'true' edge.  I've intentionally written this in a way that suggests it holds even within complex expressions, but at the very least this should work:
  if rect.dimensions matches (.height = h, .width = w) where h >= w {
    …
  }

The keyword 'matches' is not set in stone.  It's hardly even set in sand.  Clearly we should use =~. :)

Pattern grammar.

The usual syntax rule is that the pattern grammar mirrors the introduction-rule expression grammar, but with 'pattern' instead of 'expr'.  This means that, for example, if we add array literal expressions, we should also need a corresponding array literal pattern.  I think that principle is worth keeping, but leaf expressions can (and probably should) just be handled with 'case' instead of 'pattern'.

The leaf pattern is a simple variable name.  It matches everything and binds it to a new variable.  It's an error to bind the same variable twice in a single pattern;  I don't think we want to bite off contextually constrained patterns. :)  It is useful to have a special "ignore this" pattern; I suggest adopting the common convention of just assigning special semantics to the identifier '_', where it doesn't actually bind anything.
  pattern ::= identifier

This pattern is useful for binding an entire aggregate to a name while also matching on specific children.  I'm just using Haskell syntax here, which I think is nice enough.
  pattern ::= identifier '@' pattern

There's usually a pattern for annotating an arbitrary sub-pattern with a type.  I think that's less important for us because type inference is so much more constrained, but if we need it, it would be:
  pattern ::= pattern ':' type
This would then affect the parsing of vars and funcs because the (frequently mandatory) type annotations there would be parsed as part of the pattern.

We almost certainly want a pattern to test a dynamic type (including protocol satisfaction), maybe something like this:
  pattern ::= pattern 'instanceof' type
This also improves the type information in effect for checking the sub-pattern and any variables bound directly to it.

We probably do not need the following patterns for matching leaf literals;  users should just use 'case'.  This is obviously something we can provide excellent recovery for.  But non-leaf literals, like array literals, should still have patterns.
  pattern ::= numeric_constant
  pattern ::= string_constant // when we add it

Tuples are interesting because of the labelled / non-labelled distinction.  Especially with labelled elements, it is really nice to be able to ignore all the elements you don't care about.  This grammar permits some prefix or set of labels to be matched and the rest to be ignored.
  pattern ::= pattern-tuple
  pattern-tuple ::= '(' pattern-tuple-element-list? '...'? ')'
  pattern-tuple-element-list ::= pattern-tuple-element
  pattern-tuple-element-list ::= pattern-tuple-element ',' pattern-tuple-element-list
  pattern-tuple-element ::= pattern
  pattern-tuple-element ::= '.' identifier = pattern

The final cases are for ADT alternatives:
  pattern ::= pattern-ctor-name
  pattern ::= pattern-ctor-name pattern-tuple
  pattern-ctor-name ::= type-identifier '::' identifier
  pattern-ctor-name ::= ':' identifier

I am inclined to say it should be okay to match an ADT value against the bare name of a constructor for that ADT even if that constructor normally requires an argument;  i.e. this should work:
  match (x) {
  case :none: …
  case :some: …
  }
This would be particularly convenient in pattern-match expressions.

Miscellaneous.

It would be interesting to allow overloading / customization of pattern-matching.  We may find ourselves needing to do something like this to support non-fragile pattern matching anyway (if there's some set of restrictions that make it reasonable to permit that).  The obvious idea of compiling into the visitor pattern is a bit compelling, although control flow would be tricky — we'd probably need the generated code to throw an exception.  Alternatively, we could let the non-fragile type convert itself into a fragile type for purposes of pattern matching.

If we ever allow infix ADT constructors, we'll need to allow them in patterns as well.

Eventually, we will build regular expressions into the language, and we will allow them directly as patterns and even bind grouping expressions into user variables.

John.