Informally, a sound type system is one that never lies to you.
Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.
There are two parts:
- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.
- Progress: A well-typed term can be further evaluated if and only if it is not a value.
Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.
There are two parts:
- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.
- Progress: A well-typed term can be further evaluated if and only if it is not a value.