Type safety
|
|
In computer science, a programming language is type safe when the language does not permit the programmer to treat a value as a type to which it does not belong. Type safety requires that well-typed programs have no unspecified behaviour (i.e., their semantics are complete). Note that type safety is a property of the programming language, and not of the programs themselves. For example, it is possible to write a safe program in a type-unsafe language.
Robin Milner provided the following slogan to describe type safety:
- "Well-typed programs never go wrong."
At a fundamental level type safety is determined by two properties of the semantics of the programming language:
- (Type-) preservation
- "Well typedness" of programs remains invariant under the transition rules (i.e. evaluation rules or reduction rules) of the language.
- Progress
- A well typed program never gets "stuck", i.e., never gets into an undefined state where no further transitions are possible.
Note that these properties do not exist in a vacuum; they are inextricably linked to the semantics of the programming language they describe. Further note that these properties allow some leeway in the definition, since the notion of "well typed" program is part of the semantics of the programming language.
Type safety is usually a requirement for any toy language proposed in programming language research. Real languages, on the other hand, are generally too big for human-generated type-safety proofs, as they often require checking thousands of cases. Nevertheless, languages such as Standard ML have a rigorously defined semantics and have been shown to be type safe. Some other languages such as Haskell and Java are believed to be type safe. Note that regardless of the properties of the language definition, certain errors may occur at runtime due to bugs in the implementation, or in linked libraries written in other languages, rendering a given implementation type unsafe in certain circumstances.
The archetypal type-unsafe language is C because (for example) it is possible for an integer to be viewed as a function pointer, which can then be jumped to and executed, causing errors such as segmentation faults, or (more insidiously) silent failures. Even though the semantics of the C language explicitly allow for these violations of the type system (indeed, it can be critical for the performance of operating systems to be written in type-unsafe languages) the language never defines what should happen when, for example, a floating-point value is treated as a pointer.
In order for a language to be completely type safe it either needs to have garbage collection or place other restrictions on the allocation and deallocation of memory. Specifically, the language must not allow dangling pointers across structurally different types to exist. The reason is technical: suppose that a strongly typed language (like Pascal) required that allocated memory had to be explicitly released. If a dangling pointer existed that still pointed to the old memory location, it is possible that a new data structure can get allocated in the same space with the slot the dangling pointer refers to now pointing to a different type. For example, if the pointer initially pointed to a structure with an integer field, but in the new object a pointer field was allocated in the place of the integer, then the pointer field could be changed to anything simply by changing the value of the integer field (via dereferencing the dangling pointer). Because it is not specified what would happen when such a pointer is changed, the language is not type safe. Most type-safe languages satisfy these restrictions by using garbage collection to implement memory management.
Note that garbage collectors are best implemented in languages that allow pointer arithmetic, so that the library that implements the collector itself is best done in a type-unsafe language like C.
Type safety is synonymous with one of the many definitions of strong typing.
See also
Further reading
- Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002. (ISBN 0-262-16209-1) [1] (http://www.cis.upenn.edu/~bcpierce/tapl/)fr:Sūreté du typage