[PLT] Type system

**Type: **
A collection of values.
An estimate of the collection of values that a program fragment can assume during program execution.

**Untyped language: **
A language that does not have a (static) type system, or whose type system has a single type that contains all values.

**Typed language: **
A language with an associated (static) type system, whether or not types are part of the syntax.

---

**Type system: **
A collection of type rules for a typed programming language.
Same as static type system.

**Well-typed program: **
A program (fragment) that complies with the rules of a given type system.

Ill typed:
A program fragment that does not comply with the rules of a given type system.

---

**Trapped error: **
An execution error that immediately results in a fault.

**Untrapped error: **
An execution error that does not immediately result in a fault.

**Type safety: **
The property stating that programs do not cause untrapped errors.

**Safe language: **
A language where no untrapped errors can occur.

---

**Forbidden error: **
The occurrence of one of a predetermined class of execution errors;
Typically the improper application of an operation to a value, such as not(3).

**Well behaved: **
A program fragment that will not produce forbidden errors at run time.

**Type soundness: **
The property stating that programs do not cause forbidden errors.

**Strongly checked language: **
A language where no forbidden errors can occur at run time (depending on the definition of forbidden error).

**Weakly checked language: **
A language that is statically checked but provides no clear guarantee of absence of execution errors.

---

**Type rule: **
A component of a type system.
A rule stating the conditions under which a particular program construct will not cause forbidden errors.

**Typechecking: **
The process of checking a program before execution to establish its compliance with a given type system and therefore to prevent the occurrence of forbidden errors.

**Typing error: **
An error reported by a typechecker to warn against possible execution errors.

---

**Static checking: **
A collection of compile time tests, mostly consisting of typechecking.

**Statically checked language: **
A language where good behavior is determined before execution.

**Dynamic checking: **
A collection of run time tests aimed at detecting and preventing forbidden errors.

**Dynamically checked language: **
A language where good behavior is enforced during execution.

---

**Explicitly typed language: **
A typed language where types are part of the syntax.

**Implicitly typed language: **
A typed language where types are not part of the syntax.