Type Systems and Static Analysis
What is the difference between a type system and a static analysis?
Technically, a type system is a particular kind of static analysis. In practice, people use the term “static analysis” to refer to those static analyses which are not type systems. So, what constitutes a type system?
In my view, a type system is decidable, composable, predictable static analysis.
This essay focuses mainly on the use of type systems and static analyses for correctness issues. The use of static analysis for optimization and performance improvement is unquestioned and well-established.
Typechecking must be decidable. The user may be required to add annotations to a program, so long as there is a simple rule explaining where such annotations are required. Once annotated, the process of determining if the program is well-typed must be decidable.
It must be possible to check the type of an expression using only its immediate subexpressions, their types, and the list of their free variables.
This is a crucial precondition for the next requirement (predictability): it ensures that if you change a subroutine in a manner which does not alter its type, you will not break the well-typedness of any program which invokes it. It is the most basic form of “contract” between caller and callee.
If type checking fails, the type checker must always be able to explain the failure and the reason for the failure to the user.
There is a great paper A Few Billion Lines of Code Later about how unpredictable static analyses cause all sorts of problems in “real world” use that you'd never encounter in a research environment. I believe that this phenomenon explains why unpredictable analyses are so popular in academia but so rarely used for correctness in real life (compared to type systems, which are ubiquitous).
Some great quotes: