Pattern matching as the mechanism to add Code Contracts (C# vNext)

[jiggyswift]

I would like to ask if @MadsTorgersen and the C# team are considering using the new (powerful) pattern matching features as a mechanism to introduce Code Contracts to C# vNext.

Ideally the syntax would be consistent with the current pattern matching features and this would be seen as an orthogonal feature, and not something completely new as per previous attempts at integrating code contracts into the language.

Ideally we would have static analysis (or Analysers) that inform developers as they are coding if they have violated a contract.

For example, today we could write:

    int Add(int x, int y)
    {
        if ((x,y) is {x:>5, y:<10})
        {
            return x+y;
        }
        else throw new ArgumentException("Oops");
    }

It would be nice to have a code contracts feature where you can pattern match using the existing mechanisms (tuple, property, etc), as shown:

    int Add(int x, int y) where {x:>5,y:<10}
    {
        return x+y;
    }

If this contract is not matched an Exception should be thrown (this would be added by the compiler); and alternatively the syntax could allow you to specify the exception in code. But the key design of this feature would be for static analysis or an analyzer to provide warnings at compile time or via intellisense.

Pattern matching could be the light-weight mechanism we have been waiting for to implement code-contracts inside the language in an elegant and orthogonal way.

EDIT: I would add that my assumption, when calling a method with multiple parameters, is they would be implicitly wrapped in a tuple when performing the pattern matching on the right hand side.

[scottdorman]

This seems related to #2145, and also to my comment where a proposed syntax was

public void SetDelimiters(params string[]? delimiters)
{
   throw for nameof(delimiters)
   {
      ArgumentNullException when delimiters is null,
      ArgumentException => 
      {
         "Must have at least one delimiter" when delimiters.Length < 1,
         "Delimiters must not be null or empty" when delimiters.Any(d => !String.IsNullOrWhiteSpace(d),
         "Invalid delimiters" when delimiters.Any(d => d.IndexOfAny(new char[] { '\r', '\n' }) <= 0)
      }
   }
}

What I don't see in your syntax is how it would support the more complex expressions, null checks, etc. that code contracts do.

[jiggyswift]

Hi Scott. I am not proposing any syntax, and instead I am proposing that pattern matching syntax is used with whatever syntax that feature supports (which will no doubt be improved in the future). Here is valid code today with C# 9 (RC1):

var (age,name,active) = (5, "Hello", true);

var result = (age,name,active) switch {
  {age:>5 and <10, name:not null} => true,
  {name:not null} => true,
  _ => false
};

I only provide that because it compiles today (for reference). So using the first example of pattern matching for code contracts, you could write this:

void DoWork(int age, string name, bool active) where {age:>5 and <10, name:not null}
{
}

This is just using today's pattern matching syntax. I believe the C# team are more likely to embrace an orthogonal feature, even if limited. In fact, I suggest that by design, the first version of this feature guides developers to only use pattern matching and not perform arbitrary code execute (which you do in your example above). I completely understand how useful it is to perform arbitrary code execution as part of the contract, but worry that may be a step too far at least initially (realising this does already happen in a limited way inside people's getters).

[jiggyswift]

Hi @scottdorman I should also add an example that if you wanted to check the (string) name was between 5 and 10 characters long you would do this:

void DoWork(int age, string name, bool active) where {age:>5 and <10, name:{Length:>5 and <10}}
{
}

But I want to be really clear that I am not "suggested" any specific syntax here; other than just suggesting we use the current pattern matching syntax (which works in C# 9).

I suspect that whenever a solution involving arbitrary code execution is suggested, the community will not reach consensus and another decade will pass without movement on this.

[scottdorman]

I think this still suffers from the problem of not being able to support the more complex validation scenarios and the pattern matching syntax doesn't provide a good mechanism for saying what exception to throw, optionally providing the message for that exception. In your example:

• what exception is thrown when age doesn't meet the >5 and <10 criteria?
• should it throw if name is null?
• what's the exception if name doesn't meet the length criteria?

It also makes these feel more like constraints, such that the method is only valid when those criteria are met.

I think contracts, and parameter validations, should be explicit about what their intent and outcome is. The syntax I mentioned, this would look something like this:

void DoWork(int age, string name, bool active)
{
   throw for age
   {
      ArgumentNullException when name is null,
      InvalidOperation when age > 5 && age < 10,
      InvalidOperation when name.Length > 5 and name.Length < 10
   }
}

Thinking about this some more, it could be reasonable to flip things around:

void DoWork(int age, string name, bool active)
{
   throw ArgumentNullException when name is null;
   throw InvalidOperation when {age:>5 and <10};
   throw InvalidOperation when name:{Length:>5 and <10};
}

The compiler should have enough information from that to extract the parameter name. The only piece that doesn't flow as nicely is specifying the message for the exception.

[jiggyswift]

@scottdorman I prefer to stay out of the arguments about supporting more complex scenarios. But if the team agree such support should exist, the "when" keyword already does that, allowing all your example scenarios to be expressed (using syntax that already exists in the language as per C# 9). I just don't have a view on if the "when" keyword should or should not be supported (you will never get agreement on this... and I think the community will always be 50/50 split).

Your comments about allowing an exception type to be specified are very valid. Ultimately I would prefer this feature to lean in a direction where defining an exception doesn't make sense. In the same way the compiler will not let you pass an "int" to a "string" parameter; I would prefer this feature to have the compiler provide an error (or at least a warning) if you tried to pass number 4 to an integer that needed to be between 5 and 10. I do understand that this preference might be overambitious (given runtime considerations), but think the team has already achieved something similar with non-nullables.

I think we are really considering different features. I am thinking of a feature more aligned with the non-nullable support, where the compiler can - to a high degree - prove certain things. You are more thinking about the runtime reality that in real systems, these constraints will still be violated - similar to the DoStuff(string name!) proposal of automatically throwing an exception if that parameter is null. They are really different types of features. I do like your proposed syntax for the latter.

[jiggyswift]

The minimal feature would be to support the pattern matching without the "when". So you would support this:

{age:>21 and <30} and {name:{Length:>1 and <20}}

But maybe not this:

{age:>21 and <30} and {name:{Length:>1 and <20}} when name.Contains("hello") 

Supporting "when", while useful, would make it more likely developers would arbitrarily execute code as part of evaluating the contract.
Hopefully this is enough to at least start a discussion.

[JustNrik]

I would personally prefer throws... when

void SomeMethod(Foo foo)
    throws ArgumentNullException(nameof(foo)) when foo is null
{
    // translated directly to if (foo is null) throw new ArgumentNullException(nameof(foo));
}

[TheUnlocked]

throws would be interesting because it could allow multiple contract clauses which have different errors. Of course, at that point there's a question of whether the contract syntax would actually be improving legibility or making it easier to write code.

[svick]

I don't see the advantage of this syntax. Compared with what you can do today, it's not much shorter and I think it's not really clearer either.

[jiggyswift]

@svick Yes it is really only of benefit when the compiler/analyser can prove these things and immediately underline your statement DoStuff(5) noting you are violating a constraint that requires the parameter to be between 10 and 20. That's isn't done today. The feature should be built with this as the primary feature...Not just syntactic sugar for exception handing of invalid parameters.

[svick]

@jiggyswift The old Code Contracts did that without needing any special syntax. So I don't see the need fox this syntax.

[jiggyswift]

Anything can be done using a library and support tooling, yes. For example, we don't need async/await and can just use patterns and libraries. This is a suggestion to integrate the feature into the language, similar to having support for non-nullables as a language feature.

[jiggyswift]

@JustNrik I quite like that, and it does use the idea of patterns. We now, in C# 9, already have "is XXXX" and "is not XXXX" syntax with pattern matching. If we want to allow an exception to be specified, that seems like a clean enough way to do it. Note I have been using "where" instead of "when" because "when" already has a different meaning. The team use "when" to allow ad-hoc code, such as:

if (name is {Length: >5 and <10} when name.AdHocCode("Blah"))
{}

Thus I am using the syntax:

where {Length: >5 and <10} 

Because if we want to allow ad-hoc code, we then just support the when, such as:

where {Length: >5 and <10} when name.AdHocCode("Blah"))

I am not convinced "when" should be supported. I am not convinced the feature should support ad-hoc code, and suspect people smarter than me will find problems in a compiler proving these constraints in a finite time with ad-hoc code support.

[HaloFour]

Describing the rules is the easy part. It's what happens with those rules that is interesting and complicated. How are those rules encoded so that the compiler can statically check them at compile time? Does the compiler emit runtime checks to enforce those rules? Not everyone wants to incur the cost of checks on every invocation. If the compiler does emit runtime checks, what does it do if the rules are violated? Throw some exception? Fail fast?

Contracts are fraught with policy and not everyone agrees on even the basic concerns above. That's why the existing issue hasn't moved forward, not because of syntax.

[scottdorman]

That's why I've focused more on what amounts to a simpler way to write the if (!condition) { throw new Exception(); } pattern that we all have to repeatedly write, giving a simpler and clearer way to do it that should also be more easily discovered by analysis tools. It doesn't decide on the rules that are in play, but rather allows the developer to decide what conditions cause an exception and what that exception should be, which is exactly what we're doing now.

[HaloFour]

I personally don't find throw new Exception() when !condition; to be more readable or even more concise. It just moves existing syntax around.

[jiggyswift]

@HaloFour You are correct that not everyone agrees. I really started this discussion having in mind more of a code contract where the compiler would simply not let you write DoWork(5) if the parameter needed to be between 10 and 20. I was less worried about runtime concerns, and came at it from a code-correctness point of view. I can see that many people are coming at this from the point of view of a nice syntax to throw runtime exceptions based on some ad-hoc parameter validation code.

So I can see it difficult if not impossible to reach consensus on what we are even trying to achieve. If I put this up as a proposal, I will be very specific.

[scottdorman]

compiler would simply not let you write DoWork(5) if the parameter needed to be between 10 and 20.

Code contracts have never been about preventing compilation though. They've always been about runtime correctness.

[HaloFour]

Code contracts have never been about preventing compilation though. They've always been about runtime correctness.

Static checking is an important aspect of code contracts, though. Any language-integrated flavor should at least produce warnings, which can be explicitly treated as errors, just like with NRTs. Without that metadata to inform static analysis I think any code contract feature would be pretty pointless.

[scottdorman]

Absolutely. Static checking is definitely an important aspect of code contracts and a language-provided feature should support warnings in the same way NRTs do today. What I think we can accomplish, though, given the right syntax, is a way to describe the runtime checks which should be performed and provide the compiler with additional information in order to perform some of that static analysis.

That's what was nice about the old Microsoft code contracts. If you had a bunch of legacy if...throw statements, you could add Contract.EndContractBlock() at the end of them to tell the analyzer, effectively, that everything above that line are contracts. If you rewrote the contracts using the Requires class (or whichever was appropriate), the analyzer "just knew" and did the "right thing."

That's where, I think at least, having a built-in syntax to use instead of a bunch of if...throw statements would help. It allows for static analyzers to easily detect the "contract definition", as that's the only thing that would use the syntax and allows the compiler to detect what the "runtime behavior" should be and translate it into the appropriate if...throw statements. It also allows anyone reading the code to see that "these lines of code are 'special' in that they describe a series of pre-conditions that must be met" and does so in a way that makes it clear what exception will be thrown under what circumstances without (potentially) requiring the developer to write a bunch of repeated code to throw one type of exception. I can say "throw this exception under these 1..n conditions; throw this exception under these other 1..n conditions".