In computer science, type safety is a property of some programming languages that is defined differently by different communities, but most definitions involve the use of a type system to prevent certain erroneous or undesirable program behavior (called "type errors"). The formal type-theoretic definition is considerably stronger than what is understood by most programmers.
The enforcement can be static, catching potential errors at compile time, or dynamic, associating type information with values at run time and consulting them as needed to detect imminent errors, or a combination of both. Type safety is a property of the programming language, not of the programs themselves. For example, it is possible to write a safe program in a type-unsafe language.
The behaviors classified as type errors by a given programming language are usually those that result from attempts to perform an operation on some values, that is not appropriate to their data types. This classification is partly based on opinion: some language designers and programmers argue that any operation not leading to program crashes, security flaws or other obvious failures is legitimate and need not be considered an error, while others consider any contravention of the programmer's intent (as communicated via typing annotations) to be erroneous and deserving of the label "unsafe".
In the context of static 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, subtype and polymorphism for complications.
Type safety is closely linked to "memory safety", a restriction on the ability to copy arbitrary bit patterns from one memory location to another. For instance, in an implementation of a language that has some type , such that some sequence of bits (of the appropriate length) does not represent a legitimate member of , if that language allows data to be copied into a variable of type , then it is not type safe because such an operation might assign a non- value to that variable. Conversely, if the language is type unsafe to the extent of allowing an arbitrary integer to be used as a pointer, then it is clearly not memory safe.
Most statically-typed languages provide a degree of type safety that is strictly stronger than memory safety, because their type systems enforce the proper use of abstract data types defined by programmers even when this is not strictly necessary for memory safety or for the prevention of any kind of catastrophic failure.
Definitions
Robin Milner provided the following slogan to describe type safety::"Well-typed programs never go wrong."The appropriate formalization of this slogan depends on the style of formal semantics used for a particular language. In the context of denotational semantics, type safety means that the value of an expression that is well-typed, say with type τ, is a "bona fide" member of the set corresponding to τ.
In 1994, Andrew Wright and Matthias Felleisen formulated what is now the standard definition and proof technique for type safety in languages defined by operational semantics. Under this approach, 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.
These properties do not exist in a vacuum; they are linked to the semantics of the programming language they describe, and there is a large space of varied languages that can fit these criteria, since the notion of "well typed" program is part of the static semantics of the programming language and the notion of "getting stuck" (or "going wrong") is a property of its dynamic semantics.
Vijay Saraswat provides the following 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."
Type-safe and type-unsafe languages
Type safety is usually a requirement for any toy language proposed in academic programming language research. Many languages, on the other hand, 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 be meet one definition of type safetyFact|date=February 2007. On the other hand, some languages, like Java, have been proved to not meet this definition of type safety [cite web |last=Saraswat |first=Vijay | date=1997-08-15 |title=Java is not type-safe |url=http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html |accessdate=2008-10-08 ] . 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 I/O is possible, circumvents the type system and so can be used to break type safety [cite web |url=http://www.haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.html#v:unsafePerformIO |title=System.IO.Unsafe |work=GHC libraries manual: base-3.0.1.0 |accessdate=2008-07-17 ] ). Type punning is another example of such an "escape" feature. 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; such errors could render a given implementation type unsafe in certain circumstances.
Memory management in type-safe languages
To be type-safe, a language must have garbage collection or otherwise restrict the allocation and de-allocation of memory. Specifically, it must not allow dangling pointers across structurally different types. This is because if a typed language (like Pascal) required that allocated memory be explicitly released, and a dangling pointer still points to the old memory location, then a new data structure may be allocated in the same space with the slot the pointer refers to but point to a different type. For example, if the pointer initially points to a structure with an integer field, but in the new object a pointer field is allocated to the place of the integer, then the pointer field could be changed to anything 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.
Garbage collectors themselves are best implemented in languages that allow pointer arithmetic, so the library that implements the collector is best done in a type-unsafe language or a language where type safety can be deactivated. C and C++ are often used.
Type safety and strong typing
Type safety is synonymous with one of the many definitions of strong typing; but type safety and dynamic typing are mutually compatible. A dynamically typed language such as Smalltalk can be seen as a strongly-typed language with a very permissive type system where any syntactically correct program is well-typed; as long as its dynamic semantics ensures that no such program ever "goes wrong" in an appropriate sense, it satisfies the definition above and can be called type-safe.
Type safety issues in specific languages
Ada
Ada was designed to be suitable for embedded systems, device drivers and other forms of system programming, but also to encourage type safe programming. To resolve these conflicting goals, Ada confines type-unsafety to a certain set of special constructs whose names usually begin with the string Unchecked_. Unchecked_Deallocation can be effectively banned from a unit of Ada text by applying pragma Pure to this unit. It is expected that programmers will use Unchecked_ constructs very carefully and only when necessary; programs that do not use them are type safe.
The SPARK programming language is a subset of Ada eliminating all its potential ambiguities and insecurities while at the same time adding statically checked contracts to the language features available. SPARK avoids the issues with dangling pointers by disallowing allocation at run time entirely.
C
The C programming language is consideredsays who the poster child of "type-unsafe" languages. While the language definition explicitly calls out the fact that behavior of 'type-unsafe' conversions is not defined, most implementations perform conversions that programmers find useful. The widespread use of C idioms that make use of unspecified or undefined conversions has helped give it a reputation for being a type-unsafe language (the same kind of conversions can be performed in Ada using unchecked conversions, however this usage is much less common than in C).
Standard ML
SML has a rigorously defined semantics and is known to be type safe. However, some implementations of SML, including Standard ML of New Jersey (SML/NJ) and Mlton, provide libraries that offer certain unsafe operations. These facilities are often used in conjunction with those implementations' foreign function interfaces to interact with non-ML code (such as C libraries) that may require data laid out in specific ways. Another example is the SML/NJ interactive toplevel itself, which must use unsafe operations to execute ML code entered by the user.
Pascal
Pascal has had a number of type safety requirements, some of which are kept in some compilers. Where a Pascal compiler dictates "strict typing", two variables cannot be assigned to each other unless they are either compatible (such as conversion of integer to real) or assigned to the identical subtype. For example, if you have the following code fragment:
Under strict typing, a variable defined as TwoTypes is "not compatible" with DualTypes (because they are not identical, even though the components of that user defined type are identical) and an assignment of TT := DT; is illegal. An assignment of TT := TT1; would be legal because the subtypes they are defined to "are" identical. However, an assignment such as TT.Q := DT.Q; would be legal.
ee also
*datatype *type theory
References
*cite book|authorlink=Benjamin C. Pierce |last=Pierce |first=Benjamin C. |title=Types and Programming Languages |publisher=MIT Press |year=2002 |isbn=0-262-16209-1 |url=http://www.cis.upenn.edu/~bcpierce/tapl/ *cite web|title=Type Safe |work=Portland Pattern Repository Wiki |url=http://c2.com/cgi/wiki?TypeSafe *cite journal |last=Wright |first=Andrew K. |coauthors=Matthias Felleisen |title=A Syntactic Approach to Type Soundness |journal=Information and Computation |volume=115 |issue=1 |pages=38-94 |year=1994 |url=http://citeseer.ist.psu.edu/wright92syntactic.html *cite journal |first=Stavros |last=Macrakis |title=Safety and power |journal=ACM SIGSOFT Software Engineering Notes |volume=7 |issue=2 |pages=25-26 |month=April |year=1982 |url=http://portal.acm.org/citation.cfm?id=1005937.1005941 |format=requires subscription *cite web|author=Saraswat, Vijay |title=Java is not type-safe |publisher=AT&T Research |year=1997 |url=http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html
Type system — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing … Wikipedia
Type inference — Type inference, or implicit typing, refers to the ability to deduce automatically the type of a value in a programming language. It is a feature present in some strongly statically typed languages. It is often characteristic of but not limited to … Wikipedia
Safety (firearms) — This article is about the mechanical safety devices built into most firearms. For the main article about firearm safety education, see Gun safety. Close up shot of a safety of an M16A2 rifle. In firearms, a safety or safety catch is a mechanism… … Wikipedia
Type polymorphism — In computer science, polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions. A function… … Wikipedia
Safety wire — Safety wiring of two pairs of drilled head bolts Safety wire or lockwire is common in the aircraft and racing industries as an extra precaution to keep vital fasteners from unintentionally loosening and parts from falling off due to vibration or… … Wikipedia
Safety climate — is a term commonly used to describe the sum of employees’ perceptions regarding overall safety within their organization. Much debate still continues over the definition and application of safety climate as the term is still used interchangeable… … Wikipedia
Type approval — is granted to a product that meets a minimum set of regulatory, technical and safety requirements. Generally, type approval is required before a product is allowed to be sold in a particular country, so the requirements for a given product will… … Wikipedia
Type 97 grenade — Type 97 Hand Grenade A Japanese Type 97 grenade, with the safety fork still in place. Type Fragmentation hand grenade Place of origin … Wikipedia
Type 77 pistol — Type 77 Type Semi automatic pistol Place of origin PRC … Wikipedia
Safety engineering — is an applied science strongly related to systems engineering and the subset System Safety Engineering. Safety engineering assures that a life critical system behaves as needed even when pieces fail.In the real world the term safety engineering… … Wikipedia
