Are there alternatives to types for static analysis?

Question

Static typing in a programming language can be helpful for enforcing certain guarantees at compile time- but are types the only tool for this job? Are there other ways of specifying invariants?

For example, a language or environment could help enforce a guarantee regarding array length, or regarding the relationships between the inputs to a function. I just haven't heard of anything like this outside of a type system.

A related thing I was wondering about is if there are any non-declarative ways to do static analysis (types are declarative, for the most part).

Answer 1

Static type systems are a kind of static analysis, but there are many static analyses that aren’t generally encoded in type systems. For example:

• Model checking is an analysis and verification technique for concurrent systems that allows you to prove that your program is well-behaved under all possible thread interleavings.

• Data flow analysis gathers information about the possible values of variables, which can determine whether some computation is redundant, or some error is not accounted for.

• Abstract interpretation conservatively models the effects of a program, usually in such a way that the analysis is guaranteed to terminate—type checkers may be implemented in a similar manner to abstract interpreters.

• Separation logic is a program logic (used for example in the Infer analyzer) which can be used to reason about program states, and identify issues such as null pointer dereferences, invalid states, and resource leaks.

• Contract-based programming is a means of specifying preconditions, postconditions, side effects, and invariants. Ada has native support for contracts and can verify some of them statically.

Optimising compilers do many small analyses in order to build intermediate data structures for use during optimisation—such as SSA, estimates of inlining costs, instruction pairing information, and so on.

Another example of non-declarative static analysis is found in the Hack typechecker, where normal control-flow constructs can refine the type of a variable:

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

And speaking of “refining”, back in the land of type systems, refinement types (as used in LiquidHaskell) pair types with predicates that are guaranteed to hold for instances of the “refined” type. And dependent types take this further, allowing types to depend on values. The “hello world” of dependent typing is usually the array concatenation function:

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

Here, ++ takes two operands of type Vec a m and Vec a n, being vectors with element type a and lengths m and n respectively, which are natural numbers (Nat). It returns a vector with the same element type whose length is m + n. And this function proves this constraint abstractly, without knowing the specific values of m and n, so the lengths of the vectors may be dynamic.

Answer 2

@JonPurdy's answer is better, but I'd like to add a few more examples:

Obvious:

• syntax checking

• linting

Non-obvious:

• Rust enables the programmer to specify whether "bindings" are mutable, and enforces these constraints.

• This is sort-of related: some languages enable some code to be run at compile time, which means that many things that would otherwise be runtime errors can be caught at compile time. Some examples are macros and Nim language procedures marked with the compileTime pragma.

• Logic programming is basically building up a program by providing assertions.

Semi-static typing:

• Facebook's Flow enables a hybrid between dynamic and static typing. The idea is that even dynamic code is implicitly typed. Flow lets you run a server that watches your code as it runs to detect possible type errors, even if you don't type-annotate your functions.

Answer 3

Type analysis does not mean a lot.

Agda is known to have a Turing-complete type system, very different (and much more difficult to compute) than ML languages (e.g. Ocaml).