¿Existen alternativas a los tipos para el análisis estático?

La escritura estática en un lenguaje de programación puede ser útil para hacer cumplir ciertas garantías en el momento de la compilación, pero ¿son los tipos la única herramienta para este trabajo? ¿Hay otras formas de especificar invariantes?

Por ejemplo, un lenguaje o entorno podría ayudar a hacer cumplir una garantía con respecto a la longitud de la matriz, o con respecto a las relaciones entre las entradas a una función. Simplemente no he oído hablar de algo así fuera de un sistema de tipos.

Una cosa relacionada de la que me preguntaba es si hay formas no declarativas de hacer análisis estáticos (los tipos son declarativos, en su mayor parte ).

Los sistemas de tipo estático son un tipo de análisis estático, pero hay muchos análisis estáticos que generalmente no están codificados en sistemas de tipo. Por ejemplo:

• La verificación de modelos es una técnica de análisis y verificación para sistemas concurrentes que le permite probar que su programa se comporta bien bajo todos los entrelazados de hilos posibles.

• El análisis del flujo de datos recopila información sobre los posibles valores de las variables, que pueden determinar si algunos cálculos son redundantes o si no se tiene en cuenta algún error.

• La interpretación abstracta modela de manera conservadora los efectos de un programa, generalmente de tal manera que se garantiza que el análisis termine; los verificadores de tipo pueden implementarse de manera similar a los intérpretes abstractos.

• La lógica de separación es una lógica de programa (utilizada, por ejemplo, en el analizador Infer ) que se puede utilizar para razonar sobre los estados del programa e identificar problemas tales como desreferencia de puntero nulo, estados no válidos y pérdidas de recursos.

• La programación basada en contratos es un medio para especificar condiciones previas, condiciones posteriores, efectos secundarios e invariantes. Ada tiene soporte nativo para contratos y puede verificar algunos de ellos estáticamente.

Los compiladores de optimización realizan muchos análisis pequeños para construir estructuras de datos intermedios para su uso durante la optimización, como SSA, estimaciones de costos de alineación, información de emparejamiento de instrucciones, etc.

Otro ejemplo de análisis estático no declarativo se encuentra en Hack typechecker, donde las construcciones normales de flujo de control pueden refinar el tipo de una variable:

$x = get_value();
if ($x !== null) {
    $x->method();    // Typechecks because $x is known to be non-null.
} else {
    $x->method();    // Does not typecheck.
}

Y hablando de "refinamiento", en la tierra de los sistemas de tipos , los tipos de refinamiento (como se usan en LiquidHaskell ) emparejan los tipos con predicados que se garantizan para instancias del tipo "refinado". Y los tipos dependientes van más allá, permitiendo que los tipos dependan de los valores. El "hola mundo" de la tipificación dependiente suele ser la función de concatenación de matriz:

(++) : (a : Type) -> (m n : Nat) -> Vec a m -> Vec a n -> Vec a (m + n)

Aquí, ++toma dos operandos de tipo Vec a my Vec a n, siendo vectores con tipo de elemento ay longitudes my n, respectivamente, que son números naturales ( Nat). Devuelve un vector con el mismo tipo de elemento cuya longitud es m + n. Y esta función prueba esta restricción de manera abstracta, sin conocer los valores específicos de my n, por lo que las longitudes de los vectores pueden ser dinámicas.

La respuesta de @ JonPurdy es mejor, pero me gustaría agregar algunos ejemplos más:

Obvio:

• comprobación de sintaxis

• linting

No obvio:

• Rust permite que el programador especifique si los "enlaces" son mutables y aplica estas restricciones.

• Esto está relacionado de alguna manera: algunos lenguajes permiten que se ejecute algún código en tiempo de compilación, lo que significa que muchas cosas que de otro modo serían errores de tiempo de ejecución se pueden detectar en tiempo de compilación. Algunos ejemplos son macros y procedimientos de lenguaje Nim marcados con el compileTimepragma .

• La programación lógica es básicamente construir un programa proporcionando aserciones.

Escritura semiestática:

• El flujo de Facebook permite un híbrido entre tipeo dinámico y estático. La idea es que incluso el código dinámico se tipea implícitamente. Flow le permite ejecutar un servidor que vigila su código mientras se ejecuta para detectar posibles errores de tipografía, incluso si no anota sus funciones.

El análisis de tipo no significa mucho.

Se sabe que Agda tiene un sistema de tipo Turing completo, muy diferente (y mucho más difícil de calcular) que los lenguajes ML (por ejemplo, Ocaml ).