Type Patterns

[eernstg]

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.

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

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

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

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

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

// 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<int>`, binding `X` to `int`; do not match `List<String>`.
Iterable<var X extends num>

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

// Match `Map<num, num>` and bind `X` to `num`;
// match `Map<num, int>` and bind `X` to `num`;
// do not match `Map<int, num>`.
Map<var X, X>

// 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 <type>, 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:

<typePatterns> ::= <typePattern> (',' <typePattern>)*

<typePattern> ::= <functionTypePatternTails>
  | <typePatternNotFunction> <functionTypePatternTails>
  | <typePatternNotFunction>

<functionTypePatternTails> ::= <functionTypePatternTail> <functionTypePatternTails>
  | <functionTypePatternTail>

<typePatternNotFunction> ::= <typePatternNotVoidNotFunction>
  | 'void'

<functionTypePatternTail> ::=
  'Function' <typePatternParameters>? <parameterTypePatternList>

<typePatternNotVoidNotFunction> ::= <typeName> <typePatternArguments>?
  | 'Function'
  | 'var' <typeIdentifier> ('extends' <type>)?

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

<parameterTypePatternList> ::= '(' ')'
  | '(' <normalParameterTypePatterns> ',' <optionalParameterTypePatterns> ')'
  | '(' <normalParameterTypePatterns> ','? ')'
  | '(' <optionalParameterTypePatterns> ')'

<typePatternArguments> ::= '<' <typePatternList> '>'

<typePatternParameter> ::=
  <metadata> <typeIdentifier> ('extends' <typePatternNotVoid>)?

<normalParameterTypePatterns> ::=
  <normalParameterTypePattern> (',' <normalParameterTypePattern>)*

<optionalParameterTypePatterns> ::= <optionalPositionalParameterTypePatterns>
  | <namedParameterTypePatterns>

<typePatternList> ::= <typePattern> (',' <typePattern>)*

<typePatternNotVoid> ::= <functionTypePattern>
  | <typePatternNotVoidNotFunction>

<normalParameterTypePattern> ::= <patternTypedIdentifier>
  | <typePattern>

<optionalPositionalParameterTypePatterns> ::=
  '[' <normalParameterTypePatterns> ','? ']'

<namedParameterTypePatterns> ::=
  '{' <patternTypedIdentifier> (',' <patternTypedIdentifier>)* ','? '}'

<functionTypePattern> ::= <functionTypePatternTails>
  | <typePatternNotFunction> <functionTypePatternTails>

<patternTypedIdentifier> ::= <typePattern> <identifier>

We use the phrase type patterns clause for terms derived from <typePatterns>, and type pattern for terms derived from <typePattern>.

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 <typeIdentifier> 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<Up> is a superinterface of List<Up>, 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<P1, .., Pj, .., Pn> 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<P1, .., Pj, .., Pn> 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<t1, .., tj, .. tn> (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<Y1 extends B1, .. Ys extends Bs>(..., 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<Y1 extends B1, .. Ys extends Bs>(..., Pj, ...) where Pj is a type pattern that introduces X, and let t be a term of the form t0 Function<Y1 extends B1, .. Ys extends Bs>(..., 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<var X, var Y> are subtype robust. But Map<var X, X> is not, because X occurs twice; this destroys subtype robustness because we could match statically with Map<num, num>, binding X to num statically, and the run-time type could then be Map<int, num>, which is a subtype of Map<num, num> but which fails to match Map<var X, X>.

Similarly, A<var X>, B<var Y extends X> is not subtype robust because X occurs twice; this destroys subtype robustness because the run-time type could implement A<int> and B<num> (which means that matching will fail), but the static type could still have A<num> and B<num> 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<var X, var Y extends X> will only match when the dynamic type of the value of x is a subtype of Map<exactly S, exactly T> 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<List<var X>> could soundly bind X to any type when matched with List<Null>.

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<Null>) is "as close as possible" to the matching type (List<List<Null>>, 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<Null> whose static type is List<List<T>> for some T, and that method may create and return a List<List<Null>> based on the binding of X, and the returned list will then actually have the type List<List<T>>, 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<var X, X> will match Map<num, int> and bind X to num shows that this allows for a certain flexibility. But the pattern Map<X, var X> with the same type illustrates that it is possible to select a value for X (namely num) such that the given type Map<num, int> is a subtype of the type Map<num, num> 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.

[eernstg]

Yes, Map<var X, X> will only bind X, but Map<var X, var Y extends X> will bind both X and Y, so only the latter will give access to the 2nd type argument of the dynamic type of the target object at Map. For instance:

main() {
  Object map = ...; // Assume non-empty.
  if (map is Map<var X, X>) {
    X x = map.values.first; // Safe (upcast).
    map[x /*safe (same type)*/] = x; // Dynamic check on passing `x`.
  }
  if (map is Map<var X, var Y extends X>) {
    Y y = map.values.first; // Safe (same type).
    X x = y; // Safe (upcast).
    map[y /*safe (upcast)*/] = y; // Safe to pass `y`.
  }
}

But they are similar in that they will both match exactly those types S where Map<S1, S2> is a superinterface of S and S2 <: S1.

[lrhn]

The runtime type can be num, for example:

Map<var X, X> map = <num, int>{1: 1};

This assignment should succeed, implying that the type pattern match was successful.
(You can't access the X variable anywhere, but the constraint that it introduced was enforced).

[eernstg]

@lrhn already mentioned an example where we'd allow type patterns as variable type annotations (which is not a case that I've considered, but we could do that and then put X in the current scope, and note that map has static type Map<invariant X, X> such that certain dynamic checks in the subsequent code can be omitted).

Just to make it fully explicit: Yes, var X is intended to facilitate dynamic binding of a type variable to the value which is obtained by inspecting the dynamic type of a given instance, as part of the matching process.

However, it's also relevant to perform matching for a given static type with a given pattern. In particular, that's the way we'll decide whether a given extension methods is applicable or not with a given receiver expression.

The notion of being 'subtype robust' is needed with extension methods, because we wouldn't want a matching process to fail at run time. That is, we must establish the guarantee that if the static type matches then the dynamic type will also match (and we rely on the general soundness property that the dynamic type of any given instance is always a subtype of any static type we could encounter for that instance).

is it true that Map<var X extends Y, var Y extends X> will match iff
X is exactly the same as Y (that is, <num, num> will match, but <num, int> won't?

Yes, that is true. But this is not a subtype robust pattern, so you would not be able to use it to specify applicable receiver types for some extension methods. If we allow type patterns in type tests then you could use it like this:

void foo<U, V>(Map<U, V> map) {
  if (map is Map<var X extends Y, var Y extends X>) {
    // Known: `map is Map<invariant Z, invariant Z>` for some `Z`.
    // We also know `Z == X == Y`, but the type system only knows that
    // `X <: Y` and `Y <: X`, so we may need to use `X` and `Y` carefully,
    // unless we get support for invariance such that we can say it directly:
    if (map is Map<invariant X, invariant X>) {
      // It's possible that the type system won't ever be smart enough to know
      // that there is no need to generate code for the above test: It's guaranteed
      // to be true, but it will probably be checked.
      ...
    }
  }
}

[eernstg]

use [type patterns] in the "on" clause of extension methods.

For that, it's required that the type pattern is subtype robust.

extension Foo<X,Y>
    on Map<var X extends Y, var Y extends X>, X extends num, Y extends num { ... }

This is a compile-time error because the given type pattern is not subtype robust: X and Y both occur 3 times, and anything above 1 eliminates subtype robustness.

The problem is exactly what you say: We can check whether there is a match with the statically known type of any given receiver, but that doesn't provide a guarantee that a match on the dynamic type will succeed. Such a guarantee only exists with subtype robust patterns.

But for usages where we do not insist that the match must be guaranteed to succeed at run time, there is no problem:

bool foo(Map map) =>
    map is Map<var X extends Y, var Y extends X>, X extends num, Y extends num);

main() {
  foo(<num, num> {1: 1}); // True.
  foo(<int, int> {1: 1}); // True, also if we cast it to `Map<num, int>`.
  foo(<num, int>{}); // False.
}

[eernstg]

extension Foo<X,Y>
    on Map<var X extends Y, var Y extends X>, X extends num, Y extends num {
  void foo() {} // No need to use `X` or `Y`, any old method will do.
}

main() {
  Map<num, num> map = <num, int>{};
  map.foo(); // Static match succeeds, dynamic match fails.
}

So the problem is simply that we have a "no such extension method" event (similar to noSuchMethod for regular instance method invocations), and that should never be possible for a statically checked invocation of an extension method (which means: any invocation of an extension method, because they simply cannot be invoked on a receiver of type dynamic).

the "on" clause gets satisfied only if the compiler knows the exact types X and Y,

We could get this kind of knowledge if Dart is extended with invariance (#229, #214), but otherwise it would basically destroy the usefulness of such an extension (because Dart today has only few kinds of expressions whose type is exact, and it is not even specified). Because of this, I'm proposing that extensions just cannot have type patterns that aren't subtype robust.

[eernstg]

Yes, I do want to maintain a distinction here.

When a method parameter is covariant there will be a dynamic type check, and that's an unavoidable consequence of having (1) covariance for generic classes, and (2) the ability to use a type variable of the enclosing class in a contravariant position in the signature of a class member. We will probably have some sort of invariance which will make it possible to eliminate this kind of dynamic check (gradually). The invocation of operator []= that you mention has just such a check on its 2nd argument.

A member lookup is technically a different thing than a dynamic check on the type of an instance, and I think it makes sense to consider it different conceptually as well. We already have a clear and sound model for this area: A dynamic member lookup is inherently capable of failing; every other member lookup is statically safe. So if we promise that e has a foo at compile-time then e will have a foo.

If we accepted e.bar(42) at compile-time because extension Bar has a suitable bar method and the static type of e matches Bar, but at run time the extension Bar cannot be used after all (because the dynamic type of the instance obtained by evaluation of e does not match Bar's requirements), then it is as if e had a bar method statically, but it does not exist dynamically. I think the consistent treatment of this situation is to make it a compile-time error. This is different from passing an ill-typed argument to bar, because there is no bar and we never get far enough to even consider which parameter types bar could have declared, nor whether any given parameters will fit.

[eernstg]

"I acknowledge that calling extension method "foo" can fail in runtime,
but I take all blame upon myself".

Can do! (.. if we allow type patterns for promotion):

main() {
  var map = ...;
  if (x is Map<var X extends Y, var Y extends X>, X extends num, Y extends num) {
    map.foo();
  }
}

You can't really use a "testAndPromoteToNonNull" ! like operator to specify that an extension method invocation must be attempted, because we need to know at compile-time which static extension to select (at least, I certainly wouldn't want a construct which will just search all the extensions in scope and see if one of them works).

It might be useful to introduce an explicit matching test, which would specify a static extension by name and evaluate to true iff the given object matches the type pattern in the given extension:

main() {
  var map = ...;
  if (x matches Foo) map.foo();
  // Or maybe even..
  (x as Foo).foo();
}

But that's an extension that we can add on later, if it turns out to be sufficiently useful in practice.

noSuchMethod

I'm not convinced that it would be sufficiently useful. ;-)

[eernstg]

(Static overloading is the Oxycontin of programming. ;-)

[eernstg]

Scoped class extensions are intended to use type patterns and the associated matching to handle generics (that was one of the goals for having type patterns in the first place).

I worked on the proposal for doing the same thing with scoped static extension methods first, because they are a bit simpler, but the idea would be exactly the same.

extension ShortToString on Iterable<var X> {
  // Similar to `toString`, but abbreviates the elements to an ellipsis.
  String shortToString => "<$X>(...)";
}
on List<var X> {
  String shortToString => "<$X>[...]";
}
on Set<var X> {
  String shortToString => "<$X>{...}";
}

[eernstg]

I haven't worked my way through all the implications, so there might be some corner cases that we need to handle, but I expect arbitrary type patterns to be applicable to scoped class extensions (#177) as long as they are subtype robust. The example you mention should not create any problems:

extension ShortToString on Iterable<var X extends num> {
  // Similar to `toString`, but abbreviates the elements to an ellipsis.
  String shortToString => "<$X>(...)";
}
on List<var X extends num> {
  String shortToString => "<$X>[...]";
}
on Set<var X extends num> {
  String shortToString => "<$X>{...}";
}

As an example of something that would violate subtype robustness, you would not be allowed to introduce stronger constraints on subtypes:

extension Whatever on Iterable<var X> {
  bar() { ... }
}
on List<var X extends num> { // Compile-time error! See `main` to see why.
  bar() { ... }
}

main() {
  Iterable<Object> it = <String>[];
  it.bar(); // Dynamic match failure: A `List<T>` only matches when `T <: num`!
}

This is a plain subtype robustness violation, because the dynamic type List<String> fails to match, even though there is a static match (it is an Iterable<Object> statically, and that matches Iterable<var X>).