Proposal: Add completeness checking to pattern matching draft specification

[agocke]

Background

As noted in issue #180, many modern programming programs are data-focused, especially distributed applications which tend to store, manipulate, and move sets of data between different storage and computation points. One solution proposed to deal with this issue is a combination of records and pattern matching. Records provide a simple way to declare and structure the data types and pattern matching provides a way to destructure and manipulate the data.

Problem

Records provide a great way to represent the data and pattern matching provides a great way to manipulate the data, but there is currently no mechanism in the #180 proposal to ensure that the data and the logic remain in sync. The nature of records and pattern matching is that the data declaration code is often far from the data consumption code. In a distributed system it's even more likely that a single data structure will be consumed and manipulated in various parts of the code base. If the data structure is ever modified, there is currently no mechanism in the draft to alert the programmer that all instances of manipulation logic must be updated.

Solution

Add completeness checking to certain switch statements on certain record types. The core of this proposal is to provide a warning when a switch statement does not handle every possible match on a type hierarchy. This proposal features two possible designs for this idea, presented in order of increasingly intrusive modification to the language.

Design 1

This design actually features no new syntax or semantics beyond that of proposal #180. The suggestion is to create a C# type heirarchy which can be guaranteed 'complete' with existing language features. In this case, complete means that it is not possible for a new subclass of the root member of the type hierarchy, so the compiler can be sure that any and all subclasses of the chosen switching type are visible in the current compilation.

We can construct this type hierarchy in existing C# with the following rules:

1. All subclasses of the root type must be sealed, preventing any subclassing of any existing leaf types in the hierarchy.
2. All constructors of the root type must be private, prevent any subclassing of the root type.
   • As a consequence, all subclasses must be inner classes and thus must be in source in the current compilation

Here's an example of the structure of this type hierarchy:

abstract class C
{
  private C() {}
  public sealed class C_1 : C {}
  public sealed class C_2 : C {}
      ...
  public sealed class C_n : C {}
}

This guarantees that switching on an instance of type C which explicitly matches C_1...C_n has matched against every possible instance of C. The only thing which changes about the language specification is a requirement that the compiler produce a warning when not all cases are matched.

Design 2

There are a few disadvantages to Design 1:

1. The mandated structure is complicated and brittle. Forgetting to mark any of the subclasses as sealed or adding any public constructors won't produce a compiler error or warning, but the compiler will now silently skip the completeness check.
2. The structure is verbose -- most of the sealed or private markers are mostly part of the 'incantation' of completeness and are not directly related to the task at hand.
3. The relevant record instances are all nested classes, so all references require an extra layer of naming indirection.

Design 2 attempts to fix these problems by replacing much of the boiler plate with a new combination of modifiers on a type -- abstract + sealed. Under Design 2, marking the root type of a hierarchy as abstract sealed will cause the structure from Design 1 to be generated by the compiler in lowering. The following example demonstrates what the structure from Design 1 looks like with an abstract sealed type:

abstract sealed class C {}
public class C_1 : C {}
public class C_2 : C {}
   ...
public class C_n : C {}

In this case, most of the problems with Design 1 are solved, but new semantics are required to be added to the language.

[alrz]

This can be another option as well (based on Design 2):

public abstract case class C {}
public case class C_1 : C {}
public case class C_2 : C {}
   ...
public case class C_n : C {}

So case classes can only inherit from other case classes. Also, this helps to distinguish between case classes and regular ones, if they were defined in different files.

[gafter]

@alrz I don't get it. Would it be an error to extend C_1 in another assembly? Or is there some other rule that would allow the compiler to know that it sees all of the cases?

[alrz]

@gafter Quoting yourself, "It's a closed hierarchy of types" (like discriminated unions in F# but more flexible since you can inherit from other cases) so why should it be extendable in another assembly?

[gafter]

@alrz so case would mean "not extendable in another assembly"? Sort of a strange choice of keyword for that meaning.

[alrz]

@gafter Same keyword is used in Scala for exactly this purpose — implying that each case class corresponds to a case statement, I guess.

[gafter]

@alrz no, case in Scala does not restrict inheritance.

[alrz]

@gafter Yes, case has nothing to do with inheritance restriction in Scala, but my suggestion is not exactly what Scala is offering. Actually it's something in between of its syntax:

sealed abstract class C
case object C_1 extends C
case object C_2 extends C

and the proposed one:

sealed abstract class C {}
class C_1 : C {}
class C_2 : C {}

I'm trying to say that I think this is a more expressive syntax compared to above examples, for this specific use case:

abstract case class C {} // or sealed abstract case class?
case class C_1 : C {}
case class C_2 : C {}

Marking all classes with a unified keyword, indicating that these classes belong to a closed hierarchy.

PS: Although, this is just another option to consider. Except for this little concern, sealed abstract looks good to me.

[orthoxerox]

Will this support multiple levels of inheritance?

abstract sealed class C {}
abstract sealed class D : C {}
public class C_1 : C {}
public class C_2 : C {}
public class D_1 : D {}
public class D_2 : D {}

So now the compiler will look for either C, (C_1 + C_2 + D) or (C_1 + C_2 + D_1 + D_2) when checking for completeness.

[gafter]

@orthoxerox Yes, we do not plan to make one level of inheritance any more special that a second level of inheritance. The compiler will have to build a decision tree and ensure that every path reachable from the root is handled.

[orthoxerox]

@gafter great, I missed that in F#.

[gafter]

See the excellent comparison of difference languages by @jonschoning in #5154 (comment)

[dsaf]

Would C#7/8 promote having more of multiple types per file or the IDE will be capable of grouping them automatically?

[DavidArno]

As I understand this proposal, it would allow the creation of discriminated unions, such as

public abstract sealed class Option<T>
{
    class None();
    class Some<T>(T value);
}

And, because the compiler knows this is a complete hierarchy, I could pattern match as follows:

public string SomeFunction(Option<int> optionalValue) =>
    optionalValue switch
    {
        case None(): "It's a None!",
        case Some(var value): $"It's a {value}"
    };

In other words, the default (or * if we stick with that notation) case wouldn't be required.

Have I understood this correctly?

[gafter]

@DavidArno Yes, that is precisely correct.

[DavidArno]

@gafter,

Is this functionality implemented in any of the feature branches yet?

[KalitaAlexey]

I suggest ADT with the following syntax:

void Process(int | List<int> v)
{
    switch (v)
    {
        case int i:
            ProcessInt(I);
            break;
        case List<int> l:
            ProcessList(l);
    }
}

And to make ADT like type the following syntax:

// For structs
struct Type = int | bool;
// For classes or both structs and classes
class Type = int | List<int>;

Roslyn may enforce a user to write class when one of specified types is not a struct.

[svick]

@KalitaAlexey I don't think you can all that ADT, it's more like union type. In ADTs, the cases have names and can be recursive (I can't tell if your proposal would allow that or not).

[KalitaAlexey]

I like how it is done in Rust. I think we could inherit their enum ADT.
In Haskell

data Expression = Number Int
                | Add Expression Expression
                | Minus Expression
                | Mult Expression Expression
                | Divide Expression Expression

I'd like to have In C#

enum Expression {
    Number(int Number),
    Add(Expression LeftOperand, Expression RightOperand),
    Minus(Expression Expression),
    Mult(Expression LeftOperand, Expression RightOperand),
    Divide(Expression LeftOperand, Expression RightOperand),
}

And pattern matching like

void ProcessExpression(Expression expression)
{
    switch (expression)
    {
    case Expression::Number n:
        ProcessNumber(n);
        break;
    case Expression::Add a:
        ProcessAdd(a);
        break;
    case Expression::Minus m:
        ProcessMinus(m);
        break;
    case Expression::Mult m:
        ProcessMult(m);
        break;
    }
    case Expression::Divide d:
        ProcessDivide(d);
        break;
}

[HaloFour]

@KalitaAlexey #6739

[KalitaAlexey]

@HaloFour Thanks. What's the difference then?

[wekempf]

The discussion around this concept is scattered everywhere, so forgive me if I just repeat something said elsewhere. Option 1 has serious problems but is on the right track. Option 2 I don't care for because it scatters the declarations and muddles the concept. What we're modeling here is a discriminated union. @KalitaAlexey gets close to the syntax I'd prefer, but just using "enum" is at least confusing, if it doesn't actually cause parsing problem. I'd suggest (and saw others do so as well in other threads) "enum class".

public enum class Expression {
    Number(int Number),
    Add(Expression LeftOperand, Expression RightOperand),
    Minus(Expression Expression),
    Mult(Expression LeftOperand, Expression RightOperand),
    Divide(Expression LeftOperand, Expression RightOperand),
}

There's still lots of open questions after deciding on rough syntax like this, however. For instance, in this thread it was suggested a DU could have a type that's also a DU. I'm not sure that makes sense and would suggest not allowing that, knowing you can always add this feature in the future if that turns out to be the wrong decision but you can't remove a feature, ever. I just don't know when such a feature would actually be useful, and without a compelling use case it seems best to err on the conservative side.

I've seen other posts where the syntax is very similar to the above but "abstract sealed" is used instead of "enum class". Frankly, I think "abstract sealed" is highly confusing and gives no indication that one is building a DU, while "enum class" is intuitive.

[gafter]

Issue moved to dotnet/csharplang #486 via ZenHub