Strongly-typed programming language

From Wikipedia, the free encyclopedia

In computer science and computer programming, the term strong typing is used to describe those situations where programming languages specify one or more restrictions on how operations involving values having different datatypes can be intermixed. The antonym is weak typing. However, these terms have been given such a wide variety of meanings over the short history of computing that it is often difficult to know what an individual writer means by using them.

1 Interpretation
2 Meanings of Strong Typing in literature
- 2.1 Variation across programming languages
3 See also
4 References

[edit] Interpretation

Programming language expert Benjamin C. Pierce, author of Types and Programming Languages and Advanced Types and Programming Languages, has said:

"I spent a few weeks... trying to sort out the terminology of "strongly typed," "statically typed," "safe," etc., and found it amazingly difficult.... The usage of these terms is so various as to render them almost useless." ^[1]

Most generally, "strong typing" implies that the programming language places severe restrictions on the intermixing that is permitted to occur, preventing the compiling or running of source code which uses data in what is considered to be an invalid way. For instance, an integer division operation may not be used upon strings; a procedure which operates upon linked lists may not be used upon numbers. However, the nature and strength of these restrictions is highly variable.

[edit] Meanings of Strong Typing in literature

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

Static typing as opposed to dynamic typing. In a static type system, types are associated with variable names (usually when they are declared) rather than values (usually when they are created). The types may be inferred by the compiler and/or provided as annotations.
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.
Type safety; that is, the rejection (at either compile or run time) 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 disallowing of type conversion. Values of one type cannot be converted to another type, either explicitly or implicitly.
Some authors, however, reserve the phrase "strongly-typed language" for languages that omit 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 types must be converted by an explicit notation, often called a cast.
The absence of ways to evade the type system. Such evasions are possible in languages that allow programmers to get at the underlying representation of values (ie, their bit-pattern).
A complex, fine-grained type system with compound types.
Fixed and invariable typing of data objects. The type of a given data object does not vary over that object's lifetime. Class instances, for example, may not have their class altered.
Strong guarantees about the run-time behavior of a program before program execution, whether provided by static analysis or another mechanism.

[edit] Variation across programming languages

Note that some of these definitions are contradictory, while others are merely orthogonal. Because of the wide divergence among these definitions, it is possible to defend claims about most programming languages that they are either strongly- or weakly-typed. For instance:

Java, Pascal and C require all variables to have a defined type and support the use of explicit casts of arithmetic values to other arithmetic types. Java and Pascal are often said to be more strongly typed than C, a claim that is probably based on the fact that C supports more kinds of implicit conversions than Pascal and C also allows pointer values to be explicitly cast while Java & Pascal do not. Java itself may be considered more strongly typed than Pascal as manners of evading the static type system in Java are controlled by the Java Virtual Machine's dynamic type system.
OCaml or Haskell have purely static type systems, in which the compiler automatically infers a precise type for all values. Both languages are considered to have stronger type systems than Java, as they permit no type conversions at runtime. While OCaml's libraries allow one form of evasion (Object magic), this feature remains unused in most applications.
Common Lisp has a complex, fine-grained system of data types, but is almost entirely dynamically typed.
Visual BASIC is a hybrid language. In addition to including statically typed variables, it includes a "Variant" data type that can store data of any type. Its implicit casts are fairly liberal where, for example, one can sum string variants and pass the result into an integer literal.

For this reason, writers who wish to write unambiguously about type systems often eschew the term "strong typing" in favor of specific expressions such as "static typing" or "type safety".