In computer science, type safety is the extent to which a programming language discourages or prevents type errors. Type-safe languages are sometimes also called strongly or strictly typed. The behaviors classified as type errors by a given programming language are usually those that result from attempts to perform operations on values that are not of the appropriate data type, e.g. trying to add a string to an integer. Type enforcement can be static (catching potential errors at compile time), dynamic (associating type information with values at run-time and consulting them as needed to detect imminent errors), or a combination of both. Dynamic type enforcement can often run programs that would be invalid under static enforcement, but at the cost of introducing errors at runtime. In the context of static (compile-time) type systems, type safety usually involves (among other things) a guarantee that the eventual value of any expression will be a legitimate member of that expression's static type. The precise requirement is more subtle than this — see, for example, subtyping and polymorphism for complications.
Definitions Intuitively, type soundness is captured by Robin Milner's pithy statement that
Well-typed programs cannot "go wrong". In other words, if a type system is sound, then expressions accepted by that type system must evaluate to a value of the appropriate type (rather than produce a value of some other, unrelated type or crash with a type error). Vijay Saraswat provides the following, related definition:
A language is type-safe if the only operations that can be performed on data in the language are those sanctioned by the type of the data. However, what precisely it means for a program to be "well typed" or to "go wrong" are properties of its static and dynamic semantics, which are specific to each programming language. Consequently, a precise, formal definition of type soundness depends upon the style of formal semantics used to specify a language. In 1994, Andrew Wright and Matthias Felleisen formulated what has become the standard definition and proof technique for type safety in languages defined by operational semantics, which is closest to the notion of type safety as understood by most programmers. Under this approach, the semantics of a language must have the following two properties to be considered type-sound:
Progress A well-typed program never gets "stuck": every expression is either already a value or can be reduced towards a value in some well-defined way. In other words, the program never gets into an undefined state where no further transitions are possible. Preservation (or subject reduction) After each evaluation step, the type of each expression remains the same (that is, its type is preserved). A number of other formal treatments of type soundness have also been published in terms of denotational semantics and structural operational semantics.
Relation to other forms of safety In isolation, type soundness is a relatively weak property, as it essentially just states that the rules of a type system are internally consistent and cannot be subverted. However, in practice, programming languages are designed so that well-typedness also entails other, stronger properties, some of which include:
Prevention of illegal operations. For example, a type system can reject the expression 3 / "Hello, World" as invalid, because the division operator is not defined for a string divisor. Memory safety Type systems can prevent wild pointers that could otherwise arise from a pointer to one type of object being treated as a pointer to another type. More sophisticated type systems, such as those supporting dependent types, can detect and reject out-of-bound accesses, preventing potential buffer overflows. Logic errors originating in the semantics of different types. For instance, inches and millimeters may both be stored as integers, but should not be substituted for each other or added. A type system can enforce two different types of integer for them.
Type-safe and type-unsafe languages Type safety is usually a requirement for any toy language (i.e., esoteric language) proposed in academic programming language research. However, many languages are too big for human-generated type safety proofs, as they often require checking thousands of cases. Nevertheless, some languages such as Standard ML, which has rigorously defined semantics, have been proved to meet one definition of type safety. Some other languages such as Haskell are believed to meet some definition of type safety, provided certain "escape" features are not used (for example Haskell's unsafePerformIO, used to "escape" from the usual restricted environment in which input/output (I/O) is possible, circumvents the type system and so can be used to break type safety.) Type punning is another example of such an "escape" feature. Regardless of the properties of the language definition, certain errors may occur at run-time due to bugs in the implementation, or in linked libraries written in other languages; such errors could render a given implementation type unsafe in certain circumstances. An early version of Sun's Java virtual machine was vulnerable to this sort of problem.
Strong and weak typing Programming languages are often colloquially classified as strongly typed or weakly typed (also loosely typed) to refer to certain aspects of type safety. In 1974, Liskov and Zilles defined a strongly-typed language as one in which "whenever an object is passed from a calling function to a called function, its type must be compatible with the type declared in the called function." In 1977, Jackson wrote, "In a strongly typed language each data area will have a distinct type and each process will state its communication requirements in terms of these types." In contrast, a weakly typed language may produce unpredictable results or may perform implicit type conversion.
… excerpt ends here. Continue reading the full article.
