Norswap Norswap - 5 days ago 4
C# Question

Is C# type system sound and decidable?

I know that Java's type system is unsound (it fails to type check constructs that are semantically legal) and undecidable (it fails to type check some construct).

For instance, if you copy/paste the following snippet in a class and compile it, the compiler will crash with a

StackOverflowException
(how apt). This is undecidability.

static class ListX<T> {}
static class C<P> extends ListX<ListX<? super C<C<P>>>> {}
ListX<? super C<Byte>> crash = new C<Byte>();


Java uses wildcards with type bounds, which are a form of use-site variance. C# on the other hand, uses declaration site variance annotation (with the
in
and
out
keywords). It is known that declaration-site variance is weaker than use-site variance (use-site variance can express everything declaration-site variance can, and more -- on the down side, it's much more verbose).

So my question is: Is C# type system sound and decidable? If not, why?

Answer

Is C# type system sound and decidable?

It depends on what restrictions you put on the type system. Some of the C# type system's designers have a paper on the subject that you will likely find interesting:

https://www.microsoft.com/en-us/research/publication/on-decidability-of-nominal-subtyping-with-variance/

In practice, the C# 4.0 and 5.0 compilers do not implement the infinitary type detector described in the paper; rather, they go into unbounded recursion and crash.

I considered adding such code to Roslyn but do not recall a this time whether it got in or not; I'll check the source code when I'm back in my office next week.

A more gentle introduction to the problem can be found in my article here:

http://blogs.msdn.com/b/ericlippert/archive/2008/05/07/covariance-and-contravariance-part-twelve-to-infinity-but-not-beyond.aspx

UPDATE: The question asked by Andrew in the original paper -- is convertibility checking in a world with nominal subtyping and contravariant generics decidable in general? -- has recently been answered. It is not. See https://arxiv.org/abs/1605.05274. I am pleased to note that the author noticed one of my posts on the subject -- not this one -- and was inspired to attack the problem.