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, out of context, what an individual writer means when using them.
Contents |
[edit] Interpretation
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]
Luca Cardelli's article Typeful Programming describes strong typing simply as the absence of unchecked runtime type errors.[2]
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 in computer 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, 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.
- Disallowing type conversion. Values of one type cannot be converted to another type, explicitly or implicitly.
- Some authors 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 programmer access to the underlying representation of values, i.e., 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. For example, class instances 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 and 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 implicit type conversions. 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.
- Assembly language and Forth have been said to be untyped. There is no type checking; it is up to the programmer to ensure that data given to functions is of the appropriate type. Any type conversion required is explicit.
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".
[edit] See also
- Data type includes a more thorough discussion of typing issues
- Comparison of programming languages has a table of languages showing whether or not they are strongly typed
- Type system
- Type safety
