Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[patterns] How do we understand the required type of a pattern? #2783

Closed
eernstg opened this issue Jan 19, 2023 · 5 comments
Closed

[patterns] How do we understand the required type of a pattern? #2783

eernstg opened this issue Jan 19, 2023 · 5 comments
Labels
patterns Issues related to pattern matching. question Further information is requested

Comments

@eernstg
Copy link
Member

eernstg commented Jan 19, 2023

An <objectPattern> is used to perform a kind of type test (along, optionally, with a set of <patternField>s used to match the result of getter invocations on the matched object). The "head" of this construct must denote a type:

It is a compile-time error if the name does not refer to a type.

We already have some discussions (such as #2770) about the case where that type is a generic class, and no actual type arguments have been specified. The feature spec continues as follows:

Apply downwards inference from M to infer type arguments for X if needed.

(In this setting, M is the matched value type and X is the type which is denoted by the head of the pattern.)

However, I do not think there is a straightforward interpretation of such patterns where this generic class actually has a specific type argument. In other words, we might not be justified in thinking that "we always have a type argument, but it might be invisible because it's provided by a type-inference-ish step".

In particular, we can have cases where no actual type argument in the pattern will yield something that we could consider to be the type of the pattern.

The feature spec uses the phrase required type to establish the final assignability check: When all the steps have been completed (e.g., in a declaration context: computing a pattern context type schema, inferring the type of the initializing expression, and type-checking/finalizing the pattern), it is required that the initializing expression is assignable to the required type of the pattern. For example:

void main() {
  if (<int>[1] case <num>[_]); // OK, `List<int>` is assignable to `List<num>`.
}

The tricky case arises when the required type of a pattern must be a proper supertype of any type that actually describes the pattern, because the types that do describe the pattern do not have a common supertype with the same "shape":

// Assume that Dart has been extended with declaration-site variance.
class C<inout X> {}

void main() {
  Object o = C<int>();
  if (o case C()); // When does it match?
}

We can't consider the object pattern C() to be the same thing as C<T>() for any specific T, because we would (presumably) want to accept a C<S> for every possible S that satisfies the bounds of C (that is, all types), and C<T> is not a common supertype of all such types, no matter which value we've chosen for T.

So we might have to consider C() to have an existential type like ∃X. C<X>, which would be a type which covers C<S> for all S, even though that set of types doesn't have a (sufficiently useful) common supertype in the current Dart subtype hierarchy.

For the dynamic semantics, we'd want to perform a similar check (like a check against the existential type in the sense that it succeeds if there exists an S such that the matched object has type C<S> or a subtype thereof). As far as I can see, the semantics of Dart today does not include any such type test.

We can encounter a similar situation already today with function types:

typedef F<X> = X Function(X);

int intId(int i) => i;

void main() {
  Function f = intId;
  if (f case F()) print('Hurrah!');
}

In this case we might want to say that F() can match a value of type F<S> for all S, but the nearest common supertype of those types is Function.

The program is accepted by the analyzer, but the CFE encounters an unhandled exception.

Stack trace
Crash when compiling file:///usr/local/google/home/eernst/lang/dart/scratch/202301/n018.dart at character offset 65:
type '_ExplicitFunctionTypeBuilder' is not a subtype of type 'NamedTypeBuilder' of ' in type cast'

#0      TypeAliasBuilderImpl.unaliasTypeArguments (package:front_end/src/fasta/builder/type_alias_builder.dart:427:27)
#1      BodyBuilder.handleObjectPattern (package:front_end/src/fasta/kernel/body_builder.dart:8616:31)
#2      Parser.parsePrimaryPattern (package:_fe_analyzer_shared/src/parser/parser_impl.dart:9564:18)
#3      Parser.parsePattern (package:_fe_analyzer_shared/src/parser/parser_impl.dart:9371:13)
#4      Parser.parseExpressionInParenthesisRest (package:_fe_analyzer_shared/src/parser/parser_impl.dart:6390:15)
#5      Parser.ensureParenthesizedCondition (package:_fe_analyzer_shared/src/parser/parser_impl.dart:6293:13)
#6      Parser.parseIfStatement (package:_fe_analyzer_shared/src/parser/parser_impl.dart:7788:13)
#7      Parser.parseStatementX (package:_fe_analyzer_shared/src/parser/parser_impl.dart:5345:14)
#8      Parser.parseStatement (package:_fe_analyzer_shared/src/parser/parser_impl.dart:5309:20)
#9      Parser.parseFunctionBody (package:_fe_analyzer_shared/src/parser/parser_impl.dart:5214:15)
#10     DietListener.buildFunctionBody (package:front_end/src/fasta/source/diet_listener.dart:1113:14)
#11     DietListener.endTopLevelMethod (package:front_end/src/fasta/source/diet_listener.dart:376:5)
#12     Parser.parseTopLevelMethod (package:_fe_analyzer_shared/src/parser/parser_impl.dart:3676:14)
#13     Parser.parseTopLevelMemberImpl (package:_fe_analyzer_shared/src/parser/parser_impl.dart:3418:14)
#14     Parser.parseTopLevelDeclarationImpl (package:_fe_analyzer_shared/src/parser/parser_impl.dart:602:14)
#15     Parser.parseUnit (package:_fe_analyzer_shared/src/parser/parser_impl.dart:403:15)
#16     SourceLoader.buildBody (package:front_end/src/fasta/source/source_loader.dart:1266:12)
<asynchronous suspension>
#17     SourceLoader.buildBodies (package:front_end/src/fasta/source/source_loader.dart:675:7)
<asynchronous suspension>
#18     KernelTarget.buildComponent.<anonymous closure> (package:front_end/src/fasta/kernel/kernel_target.dart:608:7)
<asynchronous suspension>
#19     withCrashReporting (package:front_end/src/fasta/crash.dart:136:12)
<asynchronous suspension>
#20     _buildInternal (package:front_end/src/kernel_generator_impl.dart:206:19)
<asynchronous suspension>
#21     withCrashReporting (package:front_end/src/fasta/crash.dart:136:12)
<asynchronous suspension>
#22     generateKernel.<anonymous closure> (package:front_end/src/kernel_generator_impl.dart:48:12)
<asynchronous suspension>
#23     generateKernel (package:front_end/src/kernel_generator_impl.dart:47:10)
<asynchronous suspension>
#24     kernelForModule (package:front_end/src/api_prototype/kernel_generator.dart:100:11)
<asynchronous suspension>
#25     SingleShotCompilerWrapper.compileInternal (file:///usr/local/google/home/eernst/devel/dart/test/sdk/pkg/vm/bin/kernel_service.dart:402:11)
<asynchronous suspension>
#26     Compiler.compile.<anonymous closure> (file:///usr/local/google/home/eernst/devel/dart/test/sdk/pkg/vm/bin/kernel_service.dart:211:45)
<asynchronous suspension>
#27     _processLoadRequest (file:///usr/local/google/home/eernst/devel/dart/test/sdk/pkg/vm/bin/kernel_service.dart:872:37)
<asynchronous suspension>

The following example uses a generic function, and the outcome is basically the same:

typedef F<X> = Y Function<Y extends X>(Y);

X id<X extends num>(X n) => n;

void main() {
  Function f = id;
  if (f case F()) print('Hurrah!');
}
@eernstg eernstg added question Further information is requested patterns Issues related to pattern matching. labels Jan 19, 2023
@munificent
Copy link
Member

I'm going to merge #2784 into this issue, so copy/pasting that description here:

Given:

typedef Inv<T> = T Function(T);

Consider:

Object obj = ...
if (obj case Inv()) { ... }

What does this mean? In particular, what type argument do we infer for Inv in the object pattern? Do we infer a type? Or does that pattern just mean "check that the value has the class Inv but then doesn't actually do a full type test?

If we think of it as a class test, it's almost like we treat it as:

Object obj = ...
if (obj case Inv<var T>()) { ... }

Almost as if the case itself is generic. But we don't actually have type patterns.

If we allow this, then what happens if there is further code that expects us to now know a type, like:

Object obj = ...
if (obj case Inv() && var x) { ... }

Is there a type we can promote x to?

Or:

Object obj = ...
if (obj case Inv(call: var y)) { ... }

What is the type of y?

@leafpetersen and I talked about this some and we're currently leaning towards making this an error: If a type in an object pattern has an invariant type parameter and the matched value type doesn't give us enough context to infer a type, then it's simply an error. You either need to use a more specific matched value type (i.e. not Object in the example here), or you need to write the type argument on the pattern (i.e. case Inv<String>() or whatever). There's no way to to write a pattern that means "match Inv for any T".

In other words, I think an object pattern should always match a type, and not a family of unrelated types. Because, otherwise, you can get yourself into a place further in where you do actually need it to be a type.

@eernstg
Copy link
Member Author

eernstg commented Feb 7, 2023

I think we should insist that every list pattern and every map pattern has actual type arguments.

In the case where they are written by the developer there is no issue. When they are not given in the source code they will be obtained from the matched value type (with the usual fallbacks: if the matched value type is dynamic then a list pattern has type argument <dynamic>, a map pattern has type arguments <dynamic, dynamic>; when the matched value type is Object or some other proper supertype of List and Map which is not dynamic, the type arguments are <Object?> and <Object?, Object?>; and so on).

This means that we will refrain from trying to handle a pattern like Inv() && var x as if it allows x to have exactly the types T for which there is a type argument X such that Inv<X> is a supertype of T. Instead, we will insist that Inv() is finalised to a pattern of the form Inv<T>() for some specific T, and then it will only match those scrutinees whose type is a subtype of Inv<T> for that specific T.

@munificent and @leafpetersen, I think this is fully compatible with the approach that you mentioned.

@munificent
Copy link
Member

SGTM. Do you have any thoughts on how this should be described in the proposal? This is a little outside of my wheelhouse.

@eernstg
Copy link
Member Author

eernstg commented Feb 9, 2023

I'll create a PR. It might be possible to make it quite small.

@eernstg
Copy link
Member Author

eernstg commented Mar 23, 2023

Done in #2884.

@eernstg eernstg closed this as completed Mar 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
patterns Issues related to pattern matching. question Further information is requested
Projects
None yet
Development

No branches or pull requests

2 participants