Type-Safe Programming Language
A Type-Safe Programming Language is a programming language designed to minimize type errors (erroneous or undesirable program behaviour caused by a discrepancy between differing data types).
- Context:
- It can (typically) be a Statically-Typed Language.
- Example(s):
- Counter-Example(s):
- See: Abstract Data Type, Programming Language, Data Type, Type Theory, Type Enforcement, Compile Time, Run Time (Program Lifecycle Phase), Value (Computer Science), Expression (Programming), Subtype, Polymorphism (Computer Science).
References
2016
- (Wikipedia, 2016) ⇒ http://wikipedia.org/wiki/type_safety Retrieved:2016-3-24.
- In computer science, type safety is the extent to which a programming language discourages or prevents type errors. A type error is erroneous or undesirable program behaviour caused by a discrepancy between differing data types for the program's constants, variables, and methods (functions), e.g., treating an integer (int) as a floating-point number (float). Type safety is sometimes alternatively considered to be a property of a computer program rather than the language in which that program is written; that is, some languages have type-safe facilities that can be circumvented by programmers who adopt practices that exhibit poor type safety. The formal type-theoretic definition of type safety is considerably stronger than what is understood by most programmers.
Type 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.
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. This classification is partly based on opinion; it may imply that any operation not leading to program crashes, security flaws or other obvious failures is legitimate and need not be considered an error, or it may imply that any contravention of the programmer's explicit intent (as communicated via typing annotations) to be erroneous and not "type-safe".
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, 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 [math]\displaystyle{ t }[/math] , such that some sequence of bits (of the appropriate length) does not represent a legitimate member of [math]\displaystyle{ t }[/math] , if that language allows data to be copied into a variable of type [math]\displaystyle{ t }[/math], then it is not type-safe because such an operation might assign a non- [math]\displaystyle{ t }[/math] 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 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.
- In computer science, type safety is the extent to which a programming language discourages or prevents type errors. A type error is erroneous or undesirable program behaviour caused by a discrepancy between differing data types for the program's constants, variables, and methods (functions), e.g., treating an integer (int) as a floating-point number (float). Type safety is sometimes alternatively considered to be a property of a computer program rather than the language in which that program is written; that is, some languages have type-safe facilities that can be circumvented by programmers who adopt practices that exhibit poor type safety. The formal type-theoretic definition of type safety is considerably stronger than what is understood by most programmers.