¿Cuáles son los beneficios de seguridad de un sistema de tipos?

En JavaScript: The Good Parts por Douglas Crockford, menciona en su capítulo de herencia,

El otro beneficio de la herencia clásica es que incluye la especificación de un sistema de tipos. Esto libera principalmente al programador de tener que escribir operaciones de conversión explícitas, lo cual es algo muy bueno porque al emitir, se pierden los beneficios de seguridad de un sistema de tipos.

Entonces, antes que nada, ¿qué es realmente la seguridad? protección contra la corrupción de datos, piratas informáticos, mal funcionamiento del sistema, etc.

¿Cuáles son los beneficios de seguridad de un sistema de tipos? ¿Qué hace que un sistema de tipos sea diferente y le permita proporcionar estos beneficios de seguridad?

Los sistemas de tipos evitan errores

Los sistemas de tipos eliminan los programas ilegales. Considere el siguiente código de Python.

 a = 'foo'
 b = True
 c = a / b

En Python, este programa falla; Lanza una excepción. En un lenguaje como Java, C #, Haskell , lo que sea, ni siquiera es un programa legal. Evita por completo estos errores porque simplemente no son posibles en el conjunto de programas de entrada.

Del mismo modo, un mejor sistema de tipos descarta más errores. Si saltamos a sistemas de tipos súper avanzados, podemos decir cosas como esta:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Ahora el sistema de tipos garantiza que no haya errores de división por 0.

Que tipo de errores

Aquí hay una breve lista de qué errores pueden prevenir los sistemas de tipos

1. Errores fuera de rango
2. inyección SQL
3. Generalizando 2, muchos problemas de seguridad (para qué sirve la comprobación de manchas en Perl )
4. Errores fuera de secuencia (olvidando llamar a init)
5. Forzar el uso de un subconjunto de valores (por ejemplo, solo enteros mayores que 0)
6. Gatitos nefastos (Sí, fue una broma)
7. Errores de pérdida de precisión
8. Errores de memoria transaccional de software (STM) (esto necesita pureza, que también requiere tipos)
9. Generalizando 8, controlando los efectos secundarios
10. Invariantes sobre las estructuras de datos (¿está equilibrado un árbol binario?)
11. Olvidando una excepción o lanzando la incorrecta

Y recuerde, esto también es en tiempo de compilación . No es necesario escribir pruebas con una cobertura de código del 100% para simplemente verificar si hay errores de tipo, el compilador lo hace por usted :)

Estudio de caso: cálculo lambda mecanografiado

Muy bien, examinemos el más simple de todos los sistemas de tipo, simplemente cálculo lambda escrito .

Básicamente hay dos tipos,

Type = Unit | Type -> Type

Y todos los términos son variables, lambdas o aplicación. En base a esto, podemos probar que cualquier programa bien escrito finaliza. Nunca hay una situación en la que el programa se atasque o se repita para siempre. Esto no es demostrable en el cálculo lambda normal porque, bueno, no es cierto.

Piense en esto, podemos usar sistemas de tipos para garantizar que nuestro programa no se repita para siempre, sino genial, ¿verdad?

Desvío hacia tipos dinámicos

Los sistemas de tipo dinámico pueden ofrecer garantías idénticas a los sistemas de tipo estático, pero en tiempo de ejecución en lugar de en tiempo de compilación. En realidad, dado que es tiempo de ejecución, puedes ofrecer más información. Sin embargo, pierde algunas garantías, particularmente sobre propiedades estáticas como la terminación.

Por lo tanto, los tipos dinámicos no descartan ciertos programas, sino que enrutan programas mal formados a acciones bien definidas, como lanzar excepciones.

TLDR

Entonces, en resumen, los sistemas de tipos descartan ciertos programas. Muchos de los programas están rotos de alguna manera, por lo tanto, con los sistemas de tipos evitamos estos programas rotos.

La realidad misma está tipificada. No puede agregar longitudes a los pesos. Y si bien puede agregar pies a metros (ambos son unidades de longitud), debe escalar al menos uno de los dos. Si no lo hace, puede estrellar su misión a Marte, literalmente.

En un sistema typesafe, agregar dos longitudes expresadas en unidades diferentes habría sido un error o habría causado un lanzamiento automático.

Un sistema de tipos lo ayuda a evitar errores de codificación simples, o más bien permite que el compilador detecte esos errores por usted.

Por ejemplo, en JavaScript y Python, el siguiente problema a menudo solo se detectará en tiempo de ejecución, y dependiendo de la calidad de la prueba / rareza de la condición puede llegar a la producción:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

Si bien un lenguaje fuertemente tipado lo obligará a indicar explícitamente que aes una matriz y no le permitirá asignar un número entero. De esta manera, no hay ninguna posibilidad aque no haya tenido length, incluso en los casos más raros.

Cuanto antes en el ciclo de desarrollo de software pueda detectar un error, menos costoso será solucionarlo. Considere un error que causa que su cliente más grande o todos sus clientes pierdan datos. ¡Tal error podría ser el fin de su empresa si solo se detecta después de que los clientes reales hayan perdido datos! Es claramente menos costoso encontrar y corregir este error antes de pasarlo a producción.

Incluso para errores menos costosos, se gasta más tiempo y energía si los probadores están involucrados que si los programadores pueden encontrarlo y solucionarlo. Es más barato si no se registra en el control de origen donde otros programadores pueden crear software que se base en él. La seguridad de tipos evita que se compilen ciertas clases de errores, eliminando así casi todo el costo potencial de esos errores.

Pero esa no es toda la historia. Como lo dirá cualquiera que programe en un lenguaje dinámico, algunas veces es bueno si su programa solo se compila para que pueda probar parte de él sin obtener cada pequeño detalle para resolverlo. Existe una compensación entre seguridad y conveniencia. Las pruebas unitarias pueden mitigar parte del riesgo de usar un lenguaje dinámico, pero escribir y mantener buenas pruebas unitarias tiene su propio costo, que puede ser más alto que el de usar un lenguaje de tipo seguro.

Si está experimentando, si su código solo se usará una vez (como un informe único), o si se encuentra en una situación en la que no se molestaría en escribir una prueba unitaria de todos modos, entonces un lenguaje dinámico probablemente sea perfecto para ti. Si tiene una aplicación grande y desea cambiar una parte sin romper el resto, entonces la seguridad de tipos es un salvavidas. Los tipos de errores tipo capturas de seguridad son exactamente el tipo de errores que los humanos tienden a pasar por alto o se equivocan al refactorizar.

Introducción

La seguridad de tipos se puede lograr con lenguajes de tipo estático (compilado, verificación de tipo estático) y / o tiempo de ejecución (evaluado, verificación de tipo dinámico). Según Wikipedia, un sistema de tipo '... fuerte se describe como uno en el que no hay posibilidad de un error de tipo de tiempo de ejecución no verificado (ed Luca Cardelli). En otros escritos, la ausencia de errores de tiempo de ejecución no verificados se conoce como seguridad o tipo seguridad ... '

Seguridad - Verificación de tipo estático

Clásicamente, la seguridad de tipos ha sido sinónimo de tipeo estático, en lenguajes como C, C ++ y Haskell, que están diseñados para detectar errores de coincidencia de tipos cuando se compilan. Esto tiene el beneficio de evitar condiciones potencialmente indefinidas o propensas a errores cuando se ejecuta el programa. Esto puede ser invaluable cuando existe el riesgo de que los tipos de puntero no coincidan, por ejemplo, una situación que podría conducir a consecuencias catastróficas si no se detecta. En este sentido, la escritura estática se considera sinónimo de seguridad de la memoria.

Sin embargo, la escritura estática no es completamente segura, pero aumenta la seguridad . Incluso los sistemas de tipo estático pueden tener consecuencias catastróficas. Muchos expertos consideran que los tipos estáticos se pueden usar para escribir sistemas más robustos y menos propensos a errores (críticos).

Los lenguajes de tipo estático pueden ayudar a reducir el riesgo de pérdida de datos o pérdida de precisión en el trabajo numérico, que puede ocurrir debido a una coincidencia incorrecta o truncamiento de los tipos integrales y flotantes de doble a flotante o de coincidencia incorrecta.

Hay una ventaja en el uso de lenguajes de tipo estático para eficiencia y velocidad de ejecución. El tiempo de ejecución se beneficia de no tener que determinar los tipos durante la ejecución.

Seguridad: verificación del tipo de tiempo de ejecución

Erlang, por ejemplo, es un lenguaje declarativo de tipo, marcado dinámicamente que se ejecuta en una máquina virtual. El código de Erlang puede compilarse en bytes. Erlang se considera quizás el lenguaje disponible más importante para la misión crítica y tolerante a fallas, y se informa que Erlang tiene una confiabilidad de nueve 9 (99.9999999% o no más de 31.5 ms por año).

Ciertos idiomas, como Common Lisp, no están tipificados estáticamente, pero los tipos se pueden declarar si se desea, lo que puede ayudar a mejorar la velocidad y la eficiencia. También se debe tener en cuenta que muchos de los lenguajes interpretados más utilizados, como Python, están, debajo del ciclo de evaluación, escritos en lenguajes de tipo estático como C o C ++. Tanto Commom Lisp como Python se consideran de tipo seguro según la definición anterior.

Se pierden los beneficios de seguridad de un sistema tipo.

Entonces, antes que nada, ¿qué es realmente la seguridad? protección contra la corrupción de datos, piratas informáticos, mal funcionamiento del sistema, etc.

¿Cuáles son los beneficios de seguridad de un sistema de tipos? ¿Qué hace que un sistema de tipos sea diferente y le permita proporcionar estos beneficios de seguridad?

Siento que los sistemas de tipos tienen una visión tan negativa. Un sistema de tipos se trata más de hacer una garantía que de probar la ausencia de errores. Este último es una consecuencia del sistema de tipos. Un sistema de tipos para un lenguaje de programación es una forma de producir, en tiempo de compilación, una prueba de que un programa cumple algún tipo de especificación.

El tipo de especificación que se puede codificar como tipo depende del idioma, o más directamente, de la solidez del sistema de tipos del idioma.

El tipo más básico de especificación es una garantía sobre el comportamiento de entrada / salida de las funciones y la validez del interior de un cuerpo de función. Considere un encabezado de función

f : (Int,Int) -> String

Un buen sistema de tipos se asegurará de que f solo se aplique a los objetos que producirán un par de Int cuando se evalúe, y garantiza que f siempre produzca una cadena.

Algunas declaraciones en un lenguaje, como los bloques if-then, no tienen un comportamiento de entrada / salida; aquí el sistema de tipos garantiza que cada declaración o declaración en el bloque sea válida; es decir, aplica operaciones a objetos del tipo correcto. Estas garantías son componibles.

Además, esto da una especie de condición de seguridad de la memoria. La cita con la que está tratando es sobre casting. En algunos casos, la transmisión está bien, como transmitir una Int de 32 bits a una Int de 64 bits. Sin embargo, en general, bloquea el sistema de tipos.

Considerar

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

Debido a la conversión, x se convierte en un Int, por lo que técnicamente lo anterior hace una verificación de tipo; sin embargo, realmente vence el propósito de la verificación de tipos.

Una cosa que podría hacer un sistema de tipos diferente y mejor es rechazar los modelos (A) x donde x antes del caso es tipo B, a menos que B sea un subtipo (o subobjeto) de A. Las ideas de la teoría del subtipo se han utilizado en seguridad para eliminar la posibilidad de ataques de desbordamiento / desbordamiento de enteros.

Resumen

Un sistema de tipos es una forma de demostrar que un programa cumple con algún tipo de especificación. Los beneficios que puede proporcionar un sistema de tipos dependen de la solidez del sistema de tipos utilizado.

Una ventaja que aún no se menciona para un sistema de tipos se centra en el hecho de que muchos programas se leen más de lo que se escriben y, en muchos casos, un sistema de tipos puede permitir que se especifique una gran cantidad de información de manera concisa y fácil digerido por alguien que lee el código. Si bien los tipos de parámetros no reemplazan los comentarios descriptivos, a la mayoría de las personas les resultará más rápido leer: "int Distance;" oDistance As Int32que leer "La distancia debe ser un número entero +/- 2147483647"; pasar fracciones puede producir resultados inconsistentes ". Además, los tipos de parámetros pueden ayudar a reducir la brecha entre lo que una implementación particular de una API hace, frente a lo que las personas que llaman tienen derecho a confiar. Por ejemplo, si una implementación particular de JavaScript de una API utiliza sus parámetros de una manera que coaccionar a cualquier cadena de forma numérica, puede ser claro si las personas que llaman se les permite confiar en tal comportamiento, o si otras implementaciones de la avería API fuerza si dan cuerdas. tener un método cuyo parámetro se especifica como DoubleWould deje en claro que cualquier valor de cadena debe ser coaccionado por la persona que llama antes de pasarlo; tener un método con una sobrecarga que acepte Doubley otro que acepteString aclararía un poco que las personas que llaman con cadenas podrían pasarlas como tales.

Entonces, antes que nada, ¿qué es realmente la seguridad? ¿Protección contra la corrupción de datos, piratas informáticos, mal funcionamiento del sistema, etc.?

Todas las otras respuestas y más. En general, "seguridad de tipo" simplemente significa que ninguno de los programas que un compilador compila correctamente contendrá errores de tipo.

Ahora, ¿qué es un error de tipo? En principio, puede especificar cualquier propiedad indeseable como un error de tipo, y algunos sistemas de tipo podrán garantizar estáticamente que ningún programa tenga dicho error.

Por "propiedad" anterior, me refiero a algún tipo de proposición lógica que se aplica a su programa, por ejemplo, "todos los índices están dentro de los límites de la matriz". Otros tipos de propiedades incluyen, "todos los punteros deferenciados son válidos", "este programa no realiza ninguna E / S" o "este programa solo realiza E / S a / dev / null", etc. Casi cualquier tipo de La propiedad se puede especificar y escribir de esta manera, dependiendo de la expresividad de su sistema de tipos.

Los sistemas de tipos dependientes se encuentran entre los sistemas de tipos más generales, a través de los cuales puede aplicar prácticamente cualquier propiedad que desee. Sin embargo, no es necesariamente fácil hacerlo, ya que las propiedades sofisticadas están sujetas a cortesía incompleta de Gödel .