language icon indicating copy to clipboard operation
language copied to clipboard

Does the pattern proposal intend to make downcasts from dynamic irrefutable?

Open leafpetersen opened this issue 1 year ago • 12 comments

The pattern proposal has the following text:

Null-check, variable, list, map, record, or extractor: Irrefutable if v is assignable to the static type of p. If p is a variable pattern with no type annotation, the type is inferred from v, so it is never refutable.

I believe that the use of the word assignable here means that if v has type dynamic, then the pattern would always be considered irrefutable. For example: dynamic d = ...; (int x, String y) = (d, d);

Is this intended? Or should this be replaced with "if the static type of v is a subtype of`? If this is intended, maybe worth calling out in the proposal.

leafpetersen avatar Aug 05 '22 00:08 leafpetersen

That is what I'd intend.

Using dynamic never gives you a static failure.

dynamic d = ...; 
(int x, String y) = (d, d);

should be completely equivalent to

dynamic d = ...; 
(int x, String y) = (d as int, d as String);

It's dynamic in an int (and String) context, just like any other dynamic expression getting implicitly downcast.

lrhn avatar Aug 05 '22 11:08 lrhn

Hmm, I feel like I can come up with compelling arguments either way.

On the one hand, consider this code, which attempts to test the pattern (a, b) against a value whose static type is dynamic:

f(dynamic x) {
  switch (x) {
    case (a, b):
      print('Pair of $a and $b');
    default:
      print('Something else');
  }
}
main() {
  f('hello');
}

I think it's pretty clear that this code should print Something else. It would be a huge footgun if it instead raised an exception. The only way for this code to work as intended is for the pattern (a, b) to fail to match the string 'hello'. And if a pattern match can fail, then we should definitely be calling it a "refutable" pattern.

On the other hand, consider this code, which also attempts to test the pattern (a, b) against a value whose static type is dynamic:

f(dynamic x) {
  try {
    var (a, b) = x;
    print('Pair of $a and $b');
  } catch (_) {
    print('Something else');
  }
}
main() {
  f('hello');
}

Following @lrhn's principle that

Using dynamic never gives you a static failure.

I would expect this second program to also be valid, and also print Something else. But the only way this program is statically valid is if the pattern is considered irrefutable.

So there you have it, two programs that IMHO both seem reasonable. Both of them try to match the same pattern, (a, b), against an expression of type dynamic. The former only works if the pattern is considered refutable. The latter only works if the pattern is considered irrefutable.

If I have to choose, I guess the lesser evil would be to consider the pattern to be refutable, because then the failure mode is that the second program fails to compile, and the user is a little frustrated but they fix their code and get on with their life. Whereas if we considered the pattern to be irrefutable, then the failure mode is either (a) the first program raises an exception at runtime when given a value that it clearly looks like it should be able to handle, or (b) patterns which we call "irrefutable" actually can fail at runtime, and the cumulative effect of dictionary writers all over the world turning in their graves all over the world causes devastating earthquakes.

So unless someone can think of a way of having it both ways, I would argue for changing the spec text to if the static type of v is a subtype of.

stereotype441 avatar Aug 05 '22 14:08 stereotype441

I don't see any new issues in relying on assignability. For example, we maintain that o.whatever() checks for the existence of a member named whatever at run time, and there is no compile-time error or warning about this situation. Assuming that o has two components seems to be at the same level as assuming that o has a member named whatever.

On the other hand, we should have all kinds of diagnostic support for avoiding that the type dynamic plays a non-trivial role during static analysis. Developers would then be able to use that, effectively treating the downcast from dynamic as an error.

eernstg avatar Aug 05 '22 15:08 eernstg

I think the core issue here is the conceptual clash: When we're matching an object o with a pattern p, and the static type of the expression that yielded o is dynamic, then the matching operation is implicitly claimed to be safe: "Trust me, it will match!".

However, this may be the natural treatment of dynamic, and it may work well in a declaration, but it contradicts the purpose of performing a matching operation in a switch, because those operations are intended to wait and see until run time whether or not there is a match.

But in that case we might decide that it is simply wrong to perform matching on an expression of type dynamic, and outlaw it (or at least warn that it will always just insist on matching the first case, and throw if there is no match).

eernstg avatar Aug 05 '22 15:08 eernstg

Here's another random idea:

  • Go ahead and change the spec text to if the static type of v is a subtype of, so that (a, b) is considered refutable in a dynamic context.
  • The left hand side of a destructuring assignment is allowed to be irrefutable regardless of the right hand side.
  • The left hand side of a destructuring assignment is allowed to be refutable provided that the right hand side has static type dynamic. If the match fails, an exception will be thrown.

That way we can have our cake and eat it too: switches on dynamic behave in the expected way (if a match fails, we proceed to the next case), and destructuring assignments of dynamic do too (if the match fails, an exception is thrown). And non-dynamic code behaves exactly as it behaves today.

Tricky question: would we apply this principle recursively through nested matchers? E.g. is this code allowed?

dynamic d = ...;
var ((a, b), c) = (d, d);

stereotype441 avatar Aug 05 '22 19:08 stereotype441

A static type requirement is always satisfied by an expression of type dynamic, but it's satisfied by that expression being implicitly downcast to the required type. That happens in the RHS, before pattern matching happens.

(It's slightly misleading to say that the pattern is irrefutable. The pattern match must be irrefutable, which is why the static type of the RHS matters too. If the static type of the RHS doesn't match the pattern, it's a compile-time error.)

So, when it's a requirement for an irrefutable match in a declaration that the RHS (or a specific part of it) has a type, in order for the match to be irrefutable, and the expression has type dynamic, an implicit downcast is inserted. Then the expression does have the type it needs to have, and the declaration is irrefutable.

For a case pattern, there is no static requirement, so there is no run-time down-cast from dynamic. The value survives to the pattern match, which can the fail to match.

dynamic d = ...;
var ((a, b), c) = (d, d);

This seems clear-cut, and should be type-inferred to be equivalent to:

dynamic d = ...;
var ((a, b), c) = (d as (dynamic, dynamic), d);

lrhn avatar Aug 05 '22 20:08 lrhn

My goal is to have pattern matching consistent with the language's existing behavior. (In other words, I want to retcon Dart's existing local variable declarations and switch cases as if they had been patterns all along [mostly, there's a couple of edge cases]). Right now Dart lets you do:

dynamic d = 1;
int x = d;

And:

dynamic d = 1;
switch (d) {
  case 1: print('one');
}

In both cases, dynamic is allowed statically. In a variable declaration, it becomes an implicit downcast that throws on failure. In a case, there is no downcast that could throw. The case may just fail to match.

I think patterns should be consistent with that, so:

dynamic d = (1, 2);
var (a, b) = d;

switch (d) {
  case []: print('not matched'); // No runtime exception here.
  case (a, b): print('matched');
}

Also, yes, it should be applied recursively:

dynamic d = (1, 2);
var (a, (b, c)) = (3, d);

That's the behavior I want, and I'm guessing the behavior we're all OK with? The goal of this proposal is not to make dynamic any more or less infectious than it already is.

The next question is how the proposal models it. There are four pieces:

  1. Avoiding a compile-time error when the initializer's type is dynamic in a pattern variable declaration.

  2. Avoiding a compile-time error when the matched value's type is dynamic in a switch or pattern-if.

  3. At runtime, throwing an exception if the value doesn't match the pattern's expected type in a pattern variable declaration.

  4. At runtime, refuting the match (instead of throwing an exception) if the value doesn't match the pattern's expected type in a switch case or pattern if.

So the Cartesian product of (compile time semantics, runtime semantics) × (refutable context, irrefutable context). The proposal covers those by combining a few pieces:

  • Refutability is defined based on assignability. So if the matched value is dynamic, the patterns are considered irrefutable. This allows you to use any pattern in both refutable and irrefutable contexts without reporting a compile time error when the value's type is dynamic. That takes care of 1 and 2.

  • Patterns that perform type tests define their runtime semantics by saying that a failed type test fails the match. This is equally true when the matched value's static type is dynamic or any other supertype of the pattern's type. This takes care of 4.

  • If a pattern has a match failure and occurs in an irrefutable context, that match failure becomes a runtime exception. The proposal says:

    Refutable patterns usually occur in a context where match refutation causes execution to skip over the body of code where any variables bound by the pattern are in scope. If a pattern match failure occurs in irrefutable context, a runtime exception is thrown. This can happen when matching against a value of type dynamic, or when a list pattern in a variable declaration is matched against a list of a different length.

    In other words, even though the pattern is classified as "irrefutable" for purposes of compile-time error reporting, it still relies on the same runtime semantics that we define for using the pattern in a refutable context and then we automatically turn the match failure into a runtime exception. This avoids having to define all of the runtime semantics twice when the only difference would be match failure versus throwing an exception.

    Note that as the prose says, dynamic isn't the only way this comes into play. Another one is:

    var list = [1];
    switch (list) {
      case [a, b]: print('no'); // Failed length check is match failure.
      default: print('yes');
    }
    
    try {
      var [a, b] = list; // Failed length check match failure becomes runtime
                         // exception.
    } catch (err) {
      print('yes');
    }
    

Does that all make sense? It may be that classifying the pattern as "irrefutable" is a confusing term. All that really means is "permitted in irrefutable context". It may actually be a refutable pattern in that its runtime semantics may produce a match failure.

munificent avatar Aug 05 '22 22:08 munificent

Does that all make sense? It may be that classifying the pattern as "irrefutable" is a confusing term. All that really means is "permitted in irrefutable context". It may actually be a refutable pattern in that its runtime semantics may produce a match failure.

Sure, that works. It's slightly odd that the same pattern in two different context means something different, but doesn't bother me too deeply.

var [a, b] = list; // Failed length check match failure becomes runtime
                     // exception.

I would probably lean towards making this an error or warning myself. Why make this choice specifically here? You don't allow var x? = nullableThing right? Which is the same idea: take a pattern which refutes in a refutable context and make it throw in an irrefutable context? So what's special about lists that you silently allow that?

leafpetersen avatar Aug 05 '22 22:08 leafpetersen

It's slightly odd that the same pattern in two different context means something different, but doesn't bother me too deeply.

var [a, b] = list; // Failed length check match failure becomes runtime
                     // exception.

I would probably lean towards making this an error or warning myself. Why make this choice specifically here? You don't allow var x? = nullableThing right? Which is the same idea: take a pattern which refutes in a refutable context and make it throw in an irrefutable context? So what's special about lists that you silently allow that?

It is slightly weird... but lists are slightly weird. Users and the language seem to treat it as a programmer bug if a list doesn't have as many elements as the code expects. The return type of Iterable.[] is E and not E?. If you try to access an out of bounds elements, the compiler treats that code as statically fine, but you get a runtime exception if the list turns out to be too short. So, from the compiler's perspective, all lists are as long as needed.

I think the way list patterns behave is consistent with that behavior. And (just as with [] expressions) it is pragmatically convenient to be able to destructure lists in variable declarations using list patterns.

munificent avatar Aug 05 '22 22:08 munificent

The difference between assignement/declaration and case patterns is that the latter is a test, and the former is an assertion that this will work. In most cases, that assertion is checked statically using subtype checks. For things that cannot be checked statically, but that we still allow, a failed assertion throws, but a failed case test just rejected the case.

lrhn avatar Aug 08 '22 10:08 lrhn

As an aside,

@munificent wrote:

lists are slightly weird

I think we'll have to get some data on this. The obvious choices are the following:

var list = [1, 2, 3];

// Safe matching: Just enforce that every binding is well defined.
switch (list) {
  case [a, b, c, d]: S1; // No match, cannot bind `c` and `d`.
  case [a, b] if list.length == 2: S2; // No match, guard fails.
  case [a, b]: S3; // Match, scrutinee supports binding every variable.
  default: S4;
}

// Strict matching: Safe matching, plus an implied length guard.
switch (list) {
  case [a, b, c, d]: S1; // No match, cannot bind `c` and `d`.
  case [a, b]: S2; // No match, fails implied guard `list.length == 2`.
  case [a, b, ...]: S3; // Match, binding succeeds, and there is no implicit length guard.
  default: S4;
}

The two approaches are obviously equivalent, so we should ask people what they think is more useful and readable.

eernstg avatar Aug 08 '22 14:08 eernstg

It sounds like you all consider the matching operation on a scrutinee of type dynamic to be the same thing as a matching operation on a scrutinee of type Object?. I think that's somewhat inconsistent.

We could consider another semantics as well: A matching operation on a scrutinee of type dynamic could correspond to dynamic member invocations. This kind of matching could then use an extractor pattern like dynamic(...), in order to be able to match on the objects returned by getters. A list pattern could rely on operator [] without testing for a subtype relationship with Iterable, passing arguments 0, 1 and so on, according to the pattern. A map pattern would also rely on operator [], but passing the specified keys.

It's not a given that we want to support this kind of matching, but I do think that it is a more consistent take on what it means to match a scrutinee of type dynamic. This is also the reason why I mentioned a way out: Just make it a compile-time error to have a scrutinee of type dynamic.

eernstg avatar Aug 08 '22 15:08 eernstg

These comments are great but have diverged somewhat from the original question. I think the answer is "yes", the proposal does intend to allow implicit downcasts (which may fail and throw) in irrefutable contexts if the scrutinee has type dynamic. I think the behavior is well-specified and is intended.

I've forked the discussion of list patterns to a new issue: #2415.

As far as treating matching on dynamic to be dynamic member invocations... I don't find that very compelling. Certainly patterns that explicitly do type tests must still do type tests when the scrutinee is dynamic:

dynamic d = ...
switch (d) {
  case Foo(): // Extractor.
  case Foo f: // Typed variable.
  case foo?: // Null-check.
}

Given that, it seems like it would be confusing if list, map, and record patterns spontaneously stopped doing type tests if the scrutinee happened to be type dynamic. That just seems like extra dynamism for little user value.

munificent avatar Aug 18 '22 23:08 munificent

I'm going to go ahead and close this issue because I don't have any more action I intend to take on it, but feel free to re-open if you disagree and want to keep discussing. :)

munificent avatar Aug 24 '22 00:08 munificent