Formal assertions about the typing of programs
- Type Rules
Implicatiosn between judgements
Deductions based on type rules
A variable can assume a range of possible values, and that's the meaning of type. For example, if
booleantype, then the only possible values are
false. Typing language constructs is actually a process of classifying those constructs according to their domains. Different things have different types because they range over different domains.
- Typed Language
If a language whose constructs like vairables have limited domain, then it is a typed language, like C.
- Explicitly Typed
If types are part of the syntax.
- Implicitly Typed
If types are not part of the syntax. Type system will assign/infer types for you.
- Untyped Language
If a language whose constructs like variables do not restrict their ranges, then it is an untyped language, like Assembly, LISP, or Untyped Lambda Calculas. Or you can think of it this way: it has a single universal type, that is all possible values.
- Trapped/Untrapped Errors
Errors that cause program to stop execution immediately, are trapped errors. Errors that are initially unnoticed, and then cause unintended behavious are untrapped errors. Trapped: divide-by-zero error. Untrapped: index-out-of-bound error.
- Safe/Unsafe Language
It is a language that is untrapped-error-free. Untyped language may enforce safty by runtime checking. Typed language may do that by static type checking, or dynamic type checking, or a mix of both. (But please note, some trapped error may also be eliminated during checkings.)
- Well/Ill Typed/Behaved
The union of all untrapped-errors and some subset of trapped errors may be denoted as forbidden errors. Typed languages can ensure no forbidden errors will happen by type checking. These languages are statically checked languages. A typechecker performs such static type checking. If the program passes the check, it is well typed, o.t.w. ill typed.
- Weakly Checked
If the forbidden error definition does not cover all untrapped errors, or we say some untrapped errors may not be detected during checking, we say the language is weakly checked. C is an example because it has type casting and pointer arithmatic.
Defining Type System
- Type Soundness
If it is well-typed, then it is well-behaved. (All untrapped errors and those selected trapped errors will never happen). If within a type system, such theorem holds, we say the type system is sound.
- Type Completeness
If it is well-behaved, then it is well-typed. (This one could be harder to prove.) e.g.
if true then 1 else "I AM NOT AN INTEGER" endif.
Our goal is to design a type system that is at least sound. Some general steps of defining a type system.
- Syntax of types and terms (language constructs like expressions, statements and so on)
- Scoping rules. Map id occurence to its binding location.
- Static typing environments. That's just like the Σ we use for semantics. Here we use Γ to record the mappings from terms to types.
- Typing rules. This is to define relations between term and type, a.k.a. has-type relation. And to define relations among types, a.k.a. subtype-of and equal-type relations.
- The base case. That is to establish a has-value relation that defines the domain of a type.
It's nontrivil to prove soundness. It's generally done by induction.