Является ли система С# звуковой и разрешимой?

Я знаю, что система типа Java является необоснованной (он не может вводить проверки, которые являются семантически законными) и неразрешимым (он не может ввести проверку некоторой конструкции).

Например, если вы скопируете/вставьте следующий фрагмент в класс и скомпилируете его, компилятор сработает с StackOverflowException (как apt). Это неразрешимость.

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

Java использует подстановочные знаки с ограничениями типов, которые являются формой дисперсии использования сайта. С#, с другой стороны, использует аннотацию вариации сайта объявления (с ключевыми словами in и out). Известно, что дисперсия объявления-сайта слабее, чем дисперсия на сайте-участнике (вариация на сайте-участнике может выражать все отклонения от объявлений-сайтов, а более - в нижней части, это гораздо более подробный).

Итак, мой вопрос: Является ли система С# звуковой и разрешимой? Если нет, то почему?

Ответы

Ответ 1

Является ли система С# звуковой и разрешимой?

Это зависит от того, какие ограничения вы вводите в систему типов. Некоторые разработчики систем типа С# имеют документ по этой теме, который, вероятно, найдет интересным:

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

На практике компиляторы С# 4.0 и 5.0 не используют детектор бесконечного типа, описанный в документе; скорее, они идут в неограниченную рекурсию и крушение.

Я подумал о добавлении такого кода в Roslyn, но не помню, на этот раз он попал или нет; Я проверю исходный код, когда вернусь в свой офис на следующей неделе.

Более легкое введение в проблему можно найти в моей статье здесь:

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

ОБНОВЛЕНИЕ: Вопрос, заданный Андреем в оригинальной статье, - это проверка конвертируемости в мире с номинальным подтипированием и контравариантными генериками, которые обычно разрешимы? - недавно был дан ответ. Это не. См. https://arxiv.org/abs/1605.05274. Я рад отметить, что автор заметил один из моих сообщений по этому вопросу - не этот - и был вдохновлен атаковать проблему.

Ответ 2

Не так сложно создавать проблемы, которые С# complier не может решить за разумное время. Некоторые проблемы, с которыми он сталкивается (часто связанные с выводом типа дженериков/типов), являются NP-трудными проблемами. Эрик Липперт описывает один такой пример здесь:

class MainClass
{
    class T{}
    class F{}
    delegate void DT(T t);
    delegate void DF(F f);
    static void M(DT dt)
    {
        System.Console.WriteLine("true");
        dt(new T());
    }
    static void M(DF df)
    {
        System.Console.WriteLine("false");
        df(new F());
    }
    static T Or(T a1, T a2, T a3){return new T();}
    static T Or(T a1, T a2, F a3){return new T();}
    static T Or(T a1, F a2, T a3){return new T();}
    static T Or(T a1, F a2, F a3){return new T();}
    static T Or(F a1, T a2, T a3){return new T();}
    static T Or(F a1, T a2, F a3){return new T();}
    static T Or(F a1, F a2, T a3){return new T();}
    static F Or(F a1, F a2, F a3){return new F();}
    static T And(T a1, T a2){return new T();}
    static F And(T a1, F a2){return new F();}
    static F And(F a1, T a2){return new F();}
    static F And(F a1, F a2){return new F();}
    static F Not(T a){return new F();}
    static T Not(F a){return new T();}
    static void MustBeT(T t){}
    static void Main()
    {
        // Introduce enough variables and then encode any Boolean predicate:
        // eg, here we encode (!x3) & ((!x1) & ((x1 | x2 | x1) & (x2 | x3 | x2)))
        M(x1=>M(x2=>M(x3=>MustBeT(
          And(
            Not(x3), 
            And(
              Not(x1), 
              And(
                Or(x1, x2, x1), 
                Or(x2, x3, x2))))))));
    }
}