Le système de type C # est-il solide et décidable?

Question

Je sais que Java du type de système est malsain (il ne parvient pas à la vérification du type des constructions qui sont sémantiquement juridique) et de l'indécidable (il ne parvient pas saisir, vérifier certaines de construire).

Par exemple, si vous copiez/collez le code suivant dans une classe et le compiler, le compilateur va se planter avec un StackOverflowException (comment apt). C'est l'indécidabilité.

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

Java utilise des caractères génériques avec le type de limites, qui sont une forme d'utilisation-site de la variance. C# d'autre part, les utilisations de la déclaration de site annotation de variance (avec l' in et out mots-clés). Il est connu que la déclaration-site de la variance est plus faible qu'à l'utilisation du site de la variance (utilisation de la variance peut tout exprimer déclaration-site écart, et plus encore-sur le côté vers le bas, c'est beaucoup plus clair).

Donc ma question est: Est C# type de système de son et decidable? Si non, pourquoi?

Answer 1

Est C# type de système de son et decidable?

Cela dépend de ce que les restrictions que vous mettez sur le type de système. Certains de C# type de système, les concepteurs de disposer d'un document sur le sujet que vous trouverez probablement intéressant:

http://research.microsoft.com/en-us/um/people/akenn/generics/fool2007.pdf

Dans la pratique, le C# 4.0 et 5.0 compilateurs ne pas mettre en œuvre la infinitary type de détecteur décrite dans le document; plutôt, ils vont dans la surabondance de la récursivité et de crash.

J'ai envisagé d'ajouter ce code à Roslyn, mais ne me rappelle pas cette fois qu'il a obtenu ou non; je vais vérifier le code source quand je suis de retour dans mon bureau la semaine prochaine.

Une introduction plus douce à ce problème peut être trouvée dans mon article ici:

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

Answer 2

Il n'est pas particulièrement difficile de créer des problèmes que le compliant C # ne peut pas résoudre dans un délai raisonnable. Certains des problèmes qu'il pose (souvent liés à des génériques / inférences de type) sont des problèmes difficiles à NP. Eric Lippert en décrit un exemple ici :

 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))))))));
    }
}