c# - problemas - decidibilidad sinonimo
¿El sistema de tipo C#es sólido y decidible? (2)
Sé que el sistema de tipos de Java no es sólido (no puede verificar las construcciones que son semánticamente legales) y no se puede resolver (no puede verificar el constructo).
Por ejemplo, si copia / pega el siguiente fragmento en una clase y lo compila, el compilador se bloqueará con una StackOverflowException (cómo apt). Esto es indecidibilidad.
static class ListX<T> {}
static class C<P> extends ListX<ListX<? super C<C<P>>>> {}
ListX<? super C<Byte>> crash = new C<Byte>();
Java usa comodines con límites de tipo, que son una forma de varianza del sitio de uso. C # por otro lado, usa la anotación de la declaración del sitio de declaración (con las palabras clave de out y out ). Se sabe que la varianza del sitio de declaración es más débil que la varianza del sitio de uso (la varianza del sitio de uso puede expresar todo lo que declara la varianza del sitio, y más, en el lado negativo, es mucho más detallada).
Entonces mi pregunta es: ¿el sistema tipo C # es sólido y decidible? Si no, ¿por qué?
¿El sistema tipo C # es decidible?
Un sistema de tipo es "decidible" si el compilador en teoría siempre puede decidir si el tipo de programa se comprueba o no en tiempo definido.
Depende de qué restricciones pongas en el sistema de tipos. Algunos de los diseñadores del sistema tipo C # tienen un artículo sobre el tema que probablemente encuentres interesante:
En la práctica, los compiladores C # 4.0 y 5.0 no implementan el detector de tipo infinito descrito en el documento; más bien, entran en una recursión ilimitada y colapsan.
Consideré agregar dicho código a Roslyn, pero no recuerdo una vez si entró o no; Comprobaré el código fuente cuando regrese a mi oficina la próxima semana.
Una introducción más suave al problema se puede encontrar en mi artículo aquí:
ACTUALIZACIÓN: la pregunta formulada por Andrew en el documento original: ¿la comprobación de convertibilidad en un mundo con subtipos nominales y genéricos contravariantes decidibles en general? - ha sido respondido recientemente. No lo es. Ver https://arxiv.org/abs/1605.05274 . Me complace observar que el autor notó una de mis publicaciones sobre el tema, no esta, y se inspiró para atacar el problema.
ACTUALIZACIÓN: Un comentarista señala que respondí la pregunta sobre decidability pero no la solidez.
¿Suena el sistema de tipo C #?
Un sistema de tipo es "sólido" si se nos garantiza que un programa que comprueba los tipos en tiempo de compilación no tiene errores de tipo en el tiempo de ejecución.
No, el sistema de tipo C # no es sólido, gracias a la covarianza de matriz, mi característica menos favorita:
Giraffe[] giraffes = new[] { new Giraffe() };
Animal[] animals = giraffes; // This is legal!
animals[0] = new Tiger(); // crashes at runtime with a type error
La idea aquí es que la mayoría de los métodos que toman matrices solo leen la matriz, no la escriben y es seguro leer un animal de una serie de jirafas. Java lo permite, por lo que CLR lo permite porque los diseñadores de CLR querían poder implementar variaciones en Java. C # lo permite porque el CLR lo permite. La consecuencia es que cada vez que se escribe algo en una matriz de una clase base, el tiempo de ejecución debe verificarse para verificar que la matriz no es una matriz de una clase derivada incompatible . El caso común se vuelve más lento para que el raro caso de error pueda obtener una excepción.
Sin embargo, esto trae a colación un buen punto: C # está al menos bien definido en cuanto a las consecuencias de un error de tipo. Los errores de tipo en tiempo de ejecución producen un comportamiento sano en forma de excepciones. No es como C o C ++ donde el compilador puede y generará alegremente código que hace cosas locas arbitrariamente.
Hay algunas otras formas en que el sistema de tipo C # no es delicado por diseño.
El sistema de tipo C # no (todavía) rastrea la nulidad de los tipos de referencia. Si considera que una excepción de referencia nula es un tipo de error de tipo de tiempo de ejecución, entonces C # es muy poco sólido ya que no hace casi nada para evitar este tipo de error. Es probable que se haga un trabajo para abordar esto en C # 8, pero no será el sonido.
Muchas expresiones de conversión permiten al usuario anular el sistema de tipos y declarar "Sé que esta expresión será de un tipo más específico en tiempo de ejecución, y si estoy equivocado, lanzo una excepción". (Algunos moldes significan lo contrario: "Sé que esta expresión es de tipo X, genere código para convertirlo a un valor equivalente de tipo Y". Generalmente son seguros.) Dado que este es un lugar donde el desarrollador dice específicamente que ellos saben mejor que el sistema de tipo, uno no puede culpar al sistema de tipo por el choque resultante.
También hay un puñado de características que generan un comportamiento parecido a un lanzamiento, aunque no haya un molde en el código. Por ejemplo, si tiene una lista de animales, puede decir
foreach(Giraffe g in animals)
y si hay un tigre allí, su programa se bloqueará. Como se especifica en la especificación, el compilador simplemente inserta un molde en su nombre. (Si quieres recorrer todas las jirafas e ignorar a los tigres, eso es foreach(Giraffe g in animals.OfType<Giraffe>()) .)
- El subconjunto
unsafede C # desactiva todas las apuestas; puedes romper las reglas del tiempo de ejecución arbitrariamente con él. Al apagar un sistema de seguridad, se apaga un sistema de seguridad , por lo que no debería sorprender que C # no esté en buen estado cuando se desactiva la comprobación de la solidez.
No es particularmente difícil crear problemas que el compilador de C # no puede resolver en un tiempo razonable. Algunos de los problemas con los que se plantea (a menudo relacionado con la inferencia de genéricos / tipos) son problemas difíciles para NP. Eric Lippert describe uno de esos ejemplos aquí :
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))))))));
}
}