There’s an interesting discussion on Lambda the Ultimate on type safety. It evolved from a link to a Wired article on the inadequacy of software testing to prevent bugs.
The Wired article confused the notion of type safety with what you might call “memory safety” (i.e. languages that prevent dangling pointers, buffer overflows, unsafe casts, etc.). As part of the discussion, Scott Johnson contributed an interesting taxonomy of levels of type safety in programming languages:
Absolute type safety: Type errors are not possible in a well-formed program; the implementation guarantees that every operation on every object will succeed; else the program is not well-formed. Type erasure is possible and is often performed as a runtime optimization. The statically-typed FPLs [functional programming languages] are in this category.Nominal type safety: Type errors are not possible in a well-formed program, unless explicit “dynamic” constructs (instance_of, dynamic_cast, class introspection) are used. When type errors do occur; the behavior of the system is deterministic and it’s integrity is not compromised. Java 1.4 comes to mind (though not Java 5, due to issues with the generics implementation).
Nominal type safety with exceptions: Type errors are not possible in a well-formed program; unless explicit “type unsafe” operations are performed. Such explicit operations may, if done incorrectly, cause undefined behavior and/or violate the integrity of the programming model. Examples include C#, Eiffel, and Modula 3.
Dynamic type safety: Type errors are possible in well-formed programs (and do not require use of explicit constructs which “waive” type-checking). The behavior of the system in the presence of type errors is well-defined; programs can often productively “trap” type errors as a metaprogramming construct. Java 5 is one example; as are most dynamically-typed languages (Smalltalk, Python, Ruby, Lisp).
Superficial type safety: The system performs type-checking on programs (and rejects many improperly-typed programs as ill-formed); but the language definition contains numerous “holes” (which even experienced programmers may unwittingly stumble into) that can cause type errors to occur undetected at runtime, resulting in undefined behavior and violation of the integrity of the programming model. Examples include C and C++.
Minimal type safety: The system performs little or no type analysis, either at compile-time or runtime. Type errors may have undefined behavior and compromise system integrity. Examples include assembler, BCPL, and most Forth dialects.
Note the comment on Java 5 generics. Java 5 introduced some potential type safety issues because its implementation of generics uses type erasure rather than reification. Does this make Java 5 less type safe? Perhaps but the requirements of backward-compatibility dictated this choice as explained on Neal Gafter’s blog.
0 Responses
Stay in touch with the conversation, subscribe to the RSS feed for comments on this post.