Type Patterns

In response to #169, this is a proposal for a mechanism called _type patterns_. A type pattern _P_ may contain certain syntactic elements that introduce a new type variable (look for `var`), and it supports a check for whether a given type _matches_ the pattern _P_. It is needed for various kinds of class extensions / extension methods under consideration.

The following spells out what a type pattern is and how it works, to a level of detail which is intended to support the assumption that the concept can be given a precise definition and that usages of this concept can be sound.

## Examples

The basic construct defined in this proposal is a type patterns clause, which is a comma separated list of type patterns. Here are some examples, one per line, along with some comments giving hints about the meaning of the given construct.

```dart
// Match a single, fixed type with a type pattern.
int
List
void Function()

// Match several fixed types with a type patterns clause.
A, B
Iterable, List

// Match any type, and bind `X` to it.
var X

// Match any type `T` which satisfies `T <: C`, and bind `X` to it.
var X extends C

// Match any type of the form `Iterable` and bind `X` to `T`;
// also, e.g., match `List` and bind `X` to `T`.
Iterable

// Match any type of the form `T Function()` and bind `X` to `T`;
// also, e.g., match `T function([int])` and bind `X` to `T`.
var X Function()

// Match any type of the form `T Function(S, [int])`,
// binding `X` to `T` and `Y` to `S`;
// also, e.g., match `num Function(double, [num, num])`,
// binding `X` to `num` and `Y` to `double`.
var X Function(var Y, [int])

// Match `List`, binding `X` to `int`; do not match `List`.
Iterable

// Error: cannot introduce two type variables with the same name
// in one type patterns clause.
var X, List

// Match `Map` and bind `X` to `num`;
// match `Map` and bind `X` to `num`;
// do not match `Map`.
Map

// Error if subtype robustness required (e.g., for extension methods):
// Cannot declare a match bound in a contravariant position.
extension A on void Function(var X extends num) { ... }
```

First note that every type is also a type pattern, so it is always possible to use any particular type as a pattern. The intuition behind this is that it matches the specified type.

Next, when a type is a subtype of a type pattern which is also derivable from ``, it also matches. So `int` matches `num`, and all types match `dynamic`.

Finally, a type patterns clause containing primitive type patterns (that is, where `var` occurs) matches the types as described in the comments above, which generally means that `T` matches `P` when it is possible to extract a value for each type variable introduced by a primitive type pattern in `P` which satisfies the bounds, if any, and then `T` matches the result.

## Syntax

This proposal extends the Dart grammar with the following rules:

```
::= (',' )*

::=
|
|

::=
|

::=
| 'void'

::=
'Function' ?

::= ?
| 'Function'
| 'var' ('extends' )?

::=_T<sub>j</sub>
'<' (',' )* '>'

::= '(' ')'
| '(' ',' ')'
| '(' ','? ')'
| '(' ')'

::= '<' '>'

::=
('extends' )?

::=
(',' )*

::=
|

::= (',' )*

::=
|

::=
|

::=
'[' ','? ']'

::=
'{' (',' )* ','? '}'

::=
|

::=
```

We use the phrase _type patterns clause_ for terms derived from ``, and _type pattern_ for terms derived from ``.

Note that there is currently no way in the Dart grammar to use a type pattern or a type patterns clause; it is up to other extensions of Dart to introduce syntactic locations where these constructs can occur.

## Static Analysis

Every occurrence of a type alias _F<T₁, .. T_k>_ in a pattern is replaced by the expansion _[T₁/X₁, .. T_k/X_k]B_, where _B_ is the body of _F_ and _X_j_, 1 <= _j_ <= _k_ are the type parameters of _F_. *A non-generic type alias is covered by the case _k_ = 0.*

Let _Ps_ be a type patterns clause. For any `` _X_, it is a compile-time error if _Ps_ contains two or more primitive type patterns introducing _X_. Otherwise we say that _Ps_ _introduces_ the set of type variables that are introduced by primitive type patterns in _Ps_.

The variance of a position in a pattern is declared in the same way as for positions in a type. It is a compile-time error if a primitive type pattern with a bound occurs in a contravariant position. It is a compile-time error if a primitive type pattern occurs in an invariant position. (*We could make the latter a syntax error, but then the expansion of type aliases could introduce syntax errors, so it's simpler to allow the syntax and make it a non-syntax compile-time error.*)

Let _Ps_ of the form _P₁, .. P_k_ be a type patterns clause that introduces the type variable _X_ in _P_j_ for some _j_ in 1.._k_; it may also introduce other type variables in any of its type patterns. Let _T_ be a type. The type _S_ is the type that _corresponds to_ _X_ in _Ps_ if and only if _S_ is the type that corresponds to _X_ in _P_j_.

The notion of a type that _corresponds to_ a type variable introduced by a type pattern is defined in terms of the rules stated below. We need the special placeholders `Up` and `Down` which will be used during the computation of corresponding types, but which will never occur in the resulting bindings.

Consider the situation where we wish to determine whether a type pattern `P` matches a given type `T`. The first step taken is to substitute `Down` for every covariant occurrence of `Null` in `T`, and `Up` for every contravariant occurrence of `Null` in `T`, yielding the term `t`. In the following we will consider `Up` and `Down` as names of types. (*So `Iterable` is a superinterface of `List`, etc.*) Subsequent steps are specified in the following rules:

Let `P` be a type pattern of the form `var X` or `var X extends S`. In this case `X` _corresponds_ to `Object` with respect to (`P`, `Up`) (*note that the bound cannot exist in this case because `P` occurs in a contravariant position*), and `X` _corresponds to_ `Null` with respect to (`P`, `Down`). Let `P` be a type pattern of the form `var X` or `var X extends S`, and let `t` be a term different from `Up` and `Down`. In this case `X` _corresponds_ to `[Null/Up, Null/Down]t` with respect to (`P`, `t`).

Let `P` be a type pattern of the form `C` where `Pj` is a type pattern that introduces `X`. In this case `X` corresponds to `U` with respect to (`P`, `Up`) if `X` corresponds to `U` with respect to (`Pj`, `Up`); `X` corresponds to `U` with respect to (`P`, `Down`) if `X` corresponds to `U` with respect to (`Pj`, `Down`).

Let `P` be a type pattern of the form `C` where `Pj` is a type pattern that introduces `X`, and let `t` be a term which has a direct or indirect superinterface of the form `C` (*note that `t` then cannot be `Null`, `Up`, or `Down`*). In this case `X` corresponds to `U` with respect to (`P`, `t`) if `X` corresponds to `U` with respect to (`Pj`, `tj`).

*Note that the match cannot be with respect to (`P`, `Null`), because this implies that the original pattern had an invariant occurrence of a primitive pattern introducing `X`, and that's an error. The same argument applies in the following cases, which is the reason why matching with respect to (`P`, `Null`) is not mentioned.*

Let `P` be a type pattern of the form `P0 Function<...>(...)` where `P0` is a type pattern that introduces `X`. In this case `X` corresponds to `U` with respect to (`P`, `Up`) if `X` corresponds to `U` with respect to (`P0`, `Up`), and `X` corresponds to `U` with respect to (`P`, `Down`) if `X` corresponds to `U` with respect to (`P0`, `Down`). Let `P` be a type pattern of the form `P0 Function<...>(...)` where `P0` is a type pattern that introduces `X`, and let `t` be a term of the form `s Function<...>(...)`. In this case `X` corresponds to `U` with respect to (`P`, `t`) if `X` corresponds to `U` with respect to (`P0`, `s`). In all cases, matching has failed if the corresponding type has a free occurrence of one of `Y1..Ys`.

*Note that non-generic function types are handled by the special case where `<...>` declares zero type parameters, in which case it is omitted. We do not require that the elided parts of the function types have any particular relationships with each other, because we will apply a subtype check afterwards in order to ensure that matching only succeeds when the types are appropriately related. Similar considerations apply for similar situations below.*

Let `P` be a type pattern of the form `P0 Function(..., Pj, ...)` where `Pj` is a type pattern that introduces `X`. In this case `X` corresponds to `U` with respect to (`P`, `Up`) if `X` corresponds to `U` with respect to (`Pj`, `Down`), and `X` corresponds to `U` with respect to (`P`, `Down`) if `X` corresponds to `U` with respect to (`Pj`, `Up`). In all cases, matching has failed if the corresponding type has a free occurrence of one of `Y1..Ys`.

Let `P` be a type pattern of the form `P0 Function(..., Pj, ...)` where `Pj` is a type pattern that introduces `X`, and let `t` be a term of the form `t0 Function(..., tj, ...)`. In this case `X` corresponds to `U` with respect to (`P`, `t`) if `X` corresponds to `U` with respect to (`Pj`, `tj`). In all cases, matching has failed if the corresponding type has a free occurrence of one of `Y1..Ys`.

(*TODO: Spell out treatment of optional parameters for all forms of function type. Double-check the approach to generic function types.*)

Let _Ps_ of the form _P₁, .. P_k_ be a type patterns clause introducing type variables _X₁ .. X_s_, and _T_ a type. _T_ _matches_ _Ps_ if and only if there exist types _T₁ .. T_s_ such that, for each _j_ in 1.._s_, _T_j_ satisfies its bound, if any, and _X_j_ corresponds to _T_j_ with respect to (_Ps_, _T_), and _T_ is a subtype of _[T₁/X₁ .. T_s/X_s]P_j_ for each _j_ in 1.._k_.

*Note that "exist types" does not imply that a costly search must be performed: Each step in the matching algorithm proceeds with a subterm of the given types being matched up (except for the super-interface step, where we may need to traverse the whole superinterface graph in order to find a type which is sufficiently similar to the pattern that it is being matched against), and then type variables are bound basically by being "looked up". If that process succeeds then we have performed an amount of work that is similar to a subtype check. If it fails then such types do not exist.*

## Subtyping Property

We say that a type patterns clause _Ps_ is _subtype robust_ when none of the type variables introduced by _Ps_ occur except in the type pattern that introduces it, no primitive type pattern occurring in a contravariant position has a bound, and no primitive type pattern occurs as the return type or as a parameter type of a generic function type.

*For example, `var X` and `Map` are subtype robust. But `Map` is not, because `X` occurs twice; this destroys subtype robustness because we could match statically with `Map`, binding `X` to `num` statically, and the run-time type could then be `Map`, which is a subtype of `Map` but which fails to match `Map`.*

*Similarly, `A, B` is not subtype robust because `X` occurs twice; this destroys subtype robustness because the run-time type could implement `A` and `B` (which means that matching will fail), but the static type could still have `A` and `B` as superinterfaces.*

*Finally, `Function(var X extends num)` is not subtype robust because `X` has a bound and occurs contravariantly. This breaks subtype robustness because the static type could be `Function(num)` and the run-time type could be `Function(Object)`, and this fails to match because `X <: num` would be violated.*

We consider the following property to be likely provable: Assume that _Ps_ is a subtype robust type patterns clause and _T_ is a type such that _Ps_ matches _T_, binding its type variables _X₁ .. X_s_ to types _T₁ .. T_s_; assume that _S_ is a subtype of _T_; then _Ps_ matches _S_, binding its type variables to _S₁ .. S_s_, and for each _j_ it is guaranteed that if _X_j_ occurs covariantly in _Ps_ then _S_j <: T_j_, if _X_j_ occurs contravariantly in _Ps_ then _T_j <: S_j_. (*It is a compile-time error of _Ps_ if _X_j_ occurs invariantly.*)

## Discussion

Subtype robust type patterns clauses are particularly useful with static extension methods, because we want to ensure that a subtype will successfully match a type patterns clause whenever a supertype is known to do so, because this means that we can safely match against the dynamic type in order to obtain access to the actual values of type arguments on the receiver type.

Type patterns that are not subtype robust are particularly attractive with dynamic tests. For instance, a test that `x is Map` will only match when the dynamic type of the value of `x` is a subtype of `Map` such that `T <: S`. This means, for instance, that we can use values from this map as keys in the same map. The ability to establish such type relationships is a significant expansion of the expressive power of Dart.

The special treatment of `Null` (and, in the future, an explicit bottom type would get a similar treatment) ensures that subtypes containing `Null` will have well-defined bindings for all type variables introduced by a type patterns clause. Otherwise, the pattern `List>` could soundly bind `X` to _any_ type when matched with `List`.

In some sense that choice may seem to be unimportant, because any actual elements of the list well be the null object, so there is no way to disprove that "if this element had been a list, it's type argument would be `T`", for any `T`, but the current specification ensures that the chosen binding of `X` in the example will be such that the matched type (`List`) is "as close as possible" to the matching type (`List>`, based on the pattern and the binding of `X` to `Null`), which means that whenever a type `S` matches the pattern and is a supertype of the matched type, it is also a supertype of the matching type. This means that an extension method may be invoked on a receiver of type `List` whose static type is `List>` for some `T`, and that method may create and return a `List>` based on the binding of `X`, and the returned list will then actually have the type `List>`, no matter which `T` it is.

The notion of a 'corresponding type' for a type variable with respect to a pattern and a type has a simple intuitive interpretation: We simply "look up the actual type argument at the same position as the given type variable in the pattern".

The example where the pattern `Map` will match `Map` and bind `X` to `num` shows that this allows for a certain flexibility. But the pattern `Map` with the same type illustrates that it _is_ possible to select a value for `X` (namely `num`) such that the given type `Map` is a subtype of the type `Map` produced by the match. Still, the match fails because it only considers binding `X` to `int`. This example illustrates why it makes sense to think about the occurrence of `X` which does not have the marker `var` as a "constraint".

It would also be possible to use a pure constraint based approach where all occurrences of `X` are treated as potential sources of information about possible values of `X` (as constraints on `X`). This would be more powerful than the approach that we have actually chosen, but also considerably more complex, presumably both in the implementation and when reasoning about what it does.

We believe that the chosen approach is a useful trade-off between expressive power and complexity, because it helps keeping the complexity of the matching operation low, and it keeps the results more predictable, especially in the case where an interface type has a type argument which is used in a contravariant location in a member signature.