Strong Typing - Meanings in Computer Literature

Meanings in Computer Literature

Some of the factors which writers have qualified as "strong typing" include:

• Absence of unchecked run-time type errors. This definition comes from Luca Cardelli's article Typeful Programming. In other writing, the absence of unchecked run-time errors is referred to as safety or type safety; Tony Hoare's early papers call this property security.
• Strong guarantees about the run-time behavior of a program before program execution, whether provided by static analysis, the execution semantics of the language or another mechanism.
• Type safety; that is, at compile or run time, the rejection of operations or function calls which attempt to disregard data types. In a more rigorous setting, type safety is proved about a formal language by proving progress and preservation.
• The guarantee that a well-defined error or exceptional behavior (as opposed to an undefined behavior) occurs as soon as a type-matching failure happens at runtime, or, as a special case of that with even stronger constraints, the guarantee that type-matching failures would never happen at runtime (which would also satisfy the constraint of "no undefined behavior" after type-matching failures, since the latter would never happen anyway).
• The mandatory requirement, by a language definition, of compile-time checks for type constraint violations. That is, the compiler ensures that operations only occur on operand types that are valid for the operation. However, that is also the definition of static typing, leading some experts to state: "Static typing is often confused with StrongTyping".
• Fixed and invariable typing of data objects. The type of a given data object does not vary over that object's lifetime. For example, class instances may not have their class altered.
• The absence of ways to evade the type system. Such evasions are possible in languages that allow programmer access to the underlying representation of values, i.e., their bit-pattern.
• Omission of implicit type conversion, that is, conversions that are inserted by the compiler on the programmer's behalf. For these authors, a programming language is strongly typed if type conversions are allowed only when an explicit notation, often called a cast, is used to indicate the desire of converting one type to another.
• Disallowing any kind of type conversion. Values of one type cannot be converted to another type, explicitly or implicitly.
• A complex, fine-grained type system with compound types.
• Brian Kernighan: " each object in a program has a well-defined type which implicitly defines the legal values of and operations on the object. The language guarantees that it will prohibit illegal values and operations, by some mixture of compile- and run-time checking."