What are the safety benefits of a type system?

Question

In JavaScript: The Good Parts by Douglas Crockford, he mentions in his inheritance chapter,

The other benefit of classical inheritance is that it includes the specification of a system of types. This mostly frees the programmer from having to write explicit casting operations, which is a very good thing because when casting, the safety benefits of a type system are lost.

So first of all, what actually is safety? protection against data corruption, or hackers, or system malfunctions, etc.?

What are the safety benefits of a type system? What makes a type system different that allows it to provide these safety benefits?

Answer 1

Type systems prevent errors

Type systems eliminates illegal programs. Consider the following Python code.

 a = 'foo'
 b = True
 c = a / b

In Python, this program fails; it throws an exception. In a language like Java, C#, Haskell, whatever, this isn't even a legal program. You entirely avoid these errors because they simply aren't possible in the set of input programs.

Similarly, a better type system rules out more errors. If we jump up to super advanced type systems we can say things like this:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Now the type system guarantees that there aren't any divide-by-0 errors.

What sort of errors

Here's a brief list of what errors type systems can prevent

1. Out-of-range errors
2. SQL injection
3. Generalizing 2, many safety issues (what taint checking is for in Perl)
4. Out-of-sequence errors (forgetting to call init)
5. Forcing a subset of values to be used (for example, only integers greater than 0)
6. Nefarious kittens (Yes, it was a joke)
7. Loss-of-precision errors
8. Software transactional memory (STM) errors (this needs purity, which also requires types)
9. Generalizing 8, controlling side effects
10. Invariants over data structures (is a binary tree balanced?)
11. Forgetting an exception or throwing the wrong one

And remember, this is also at compile time. No need to write tests with 100% code coverage to simply check for type errors, the compiler just does it for you :)

Case study: Typed lambda calculus

Alright, let's examine the simplest of all type systems, simply typed lambda calculus.

Basically there are two types,

Type = Unit | Type -> Type

And all terms are either variables, lambdas, or application. Based on this, we can prove that any well typed program terminates. There is never a situation where the program will get stuck or loop forever. This isn't provable in normal lambda calculus because well, it isn't true.

Think about this, we can use type systems to guarentee that our program doesn't loop forever, rather cool right?

Detour into dynamic types

Dynamic type systems can offer identical guarantees as static type systems, but at runtime rather than compile time. Actually, since it's runtime, you can actually offer more information. You lose some guarantees however, particularly about static properties like termination.

So dynamic types don't rule out certain programs, but rather route malformed programs to well-defined actions, like throwing exceptions.

TLDR

So the long and the short of it, is that type systems rule out certain programs. Many of the programs are broken in some way, therefore, with type systems we avoid these broken programs.

Answer 2

Reality itself is typed. You can't add lengths to weights. And while you can add feets to meters (both are units of lengths), you should scale at least one of the two. Failing to do so can crash your Mars mission, quite literally.

In a typesafe system, adding two lengths expressed in different units would have been either an error or would have caused an automatic cast.

Answer 3

A type system helps you avoid simple coding errors, or rather allows the compiler catch those errors for you.

For example, in JavaScript and Python, the following problem will often only be caught at runtime - and depending on testing quality/rarity of the condition may actually make it to production:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

While a strongly-typed language will force you to explicitly state that a is an array and will not let you assign an integer. In this way, there isn't any chance a won't have length - even in the rarest cases.

Answer 4

The earlier in the software development cycle you can catch an error, the less expensive it is to fix. Consider an error that causes your biggest client, or all your clients to lose data. Such an error could be the end of your company if it is only caught after real customers have lost data! It is clearly less expensive to find and fix this bug before moving it to production.

Even for less costly errors, more time and energy is spent if testers are involved than if programmers can find and fix it. It's cheaper if it does not get checked into source control where other programmers can build software that relies on it. Type safety prevents certain classes of errors from even compiling, thus eliminating almost the entire potential cost of those errors.

But that isn't the whole story. As anyone who programs in a dynamic language will tell you, some times it's nice if your program just compiles so you can try out part of it without getting every little detail to work out. There is a trade-off between safety and convenience. Unit tests can mitigate some of the risk of using a dynamic language, but writing and maintaining good unit tests has its own cost which may be higher than that of using a type-safe language.

If you are experimenting, if your code will only be used once (such as a one-time report), of if you are in a situation where you wouldn't bother to write a unit test anyway, then a dynamic language is probably perfect for you. If you have a large application and want to change one part without breaking the rest of it, then type safety is a life saver. The types of errors type safety catches are exactly the kind of errors that humans tend to overlook or get wrong when refactoring.

Answer 5

Introduction

Type safety can be achieved with either statically-typed (compiled, static type checking) and/or runtime (evaluated, dynamic type checking) languages. According to Wikipedia a '... strong type system is described as one in which there is no possibility of an unchecked runtime type error (ed Luca Cardelli). In other writing, the absence of unchecked run-time errors is referred to as safety or type safety ...'

Safety - Static Type Checking

Classically, type safety has been synonymous with static typing, in languages such as C, C++ and Haskell, that are designed to detect type mis-matches when they are compiled. This has the benefit of avoiding potentially undefined or error-prone conditions when the programme is executed. This can be invaluable where there is a risk that pointer types may be mis-matched, for example, a situation that could lead to catastrophic consequences if not detected. In this sense static typing is considered synonymous with memory safety.

Static typing is not completely safe but enhances safety, however. Even statically-typed systems can have catastrophic consequences. Many experts consider that statically-typed can be used to write more robust and less error-prone (mission critical) systems.

Statically-typed languages can help to reduce the risk of loss of data or loss of accuracy in numerical work, that can occur due to mis-matching or truncating double to float or mis-matching integral and float types.

There is an advantage in using statically-typed languages for efficiency and speed of execution. The runtime benefits from not having to determine the types during execution.

Safety - Runtime Type Checking

Erlang, for example, is a type declarative, dynamically type checked language that runs on a virtual machine. Erlang code can be byte compiled. Erlang is considered perhaps the most important mission-critical, fault tolerant language available, and it is reported that Erlang has a reliability of nine 9's (99.9999999% or not more than 31.5 msecs per year).

Certain languages, such as Common Lisp, are not statically-typed but types can be declared if desired which can help improve speed and efficiency. It is also to be noted that many of the more widely used interpreted languages, such as Python, are, underneath the evaluation loop, written in statically-typed languages such as C or C++. Both Commom Lisp and Python are considered type safe by the definition above.

Answer 6

the safety benefits of a type system are lost.

So first of all, what actually is safety? protection against data corruption, or hackers, or system malfunctions, etc.?

What are the safety benefits of a type system? What makes a type system different that allows it to provide these safety benefits?

I feel like type systems have such a negative view. A type system is more about making a guarantee than about proving the absence of errors. The latter is a consequence of the type system. A type system for a programming language is a way to produce, at compile time, a proof that a program meets some kind of specification.

The kind of specification that one can encode as a type depends on the language, or more directly, on the strength of the language's type system.

The most basic kind of specification is a guarantee about the input/output behaviour of functions and of the validity of the inside of a function body. Consider a function header

f : (Int,Int) -> String

A good type system will make sure that f is only applied to objects that will produce a pair of Int when evaluate, and guarantees that f will always produce a string.

Some statements in a language, like if-then blocks, don't have an input/output behaviour; here the type system guarantees that each declaration or statement in the block is valid; that is applies operations to objects of the correct kind. These guarantees are composable.

Also, this does give a sort of memory safety condition. The quote you are dealing with is about casting. In some cases, casting is fine, like casting a 32-bit Int to a 64-bit Int. However, generally, it does crash the type system.

Consider

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

Because of casting, x is turned into an Int, so technically the above does type check; however, it really does defeat the purpose of typechecking.

One thing that could make a different and better type system is to dissallow casts (A)x where x before the case is type B, unless B is a subtype (or subobject) of A. The ideas of subtyping theory have been used in security to remove the possibility of integer overflow/underflow attacks.

Summary

A type system is a way to prove a program meets some kind of specification. The benefits a type system can provide depend on the strength of the type system used.

Answer 7

One advantage not yet mentioned for a type system centers around the fact that many programs are read more than they are written, and in many cases a type system may allow a lot of information to be specified in a manner which is concise and can be easily digested by someone reading the code. While parameter types don't take the place of descriptive comments, most people will find it faster to read: "int Distance;" or Distance As Int32 than to read "Distance must be a whole number +/- 2147483647"; passing fractions may yield inconsistent results." Further, parameter types can help reduce the gap between what a particular implementation of an API happens to do, versus what callers are entitled to rely upon. For example, if a particular Javascript implementation of an API uses its parameters in a way which would coerce any strings to numeric form, it may be unclear whether callers are allowed to rely upon such behavior, or if other implementations of the API might malfunction if given strings. Having a method whose parameter is specified as Double would make it clear that any string values must be coerced by the caller before being passed; having a method with an overload that accepts Double and another that accepts String would make it somewhat clearer that callers holding strings would be allowed to pass them as such.

Answer 8

So first of all, what actually is safety? Protection against data corruption, or hackers, or system malfunctions, etc.?

All of the other answers and more. In general, "type safety" simply means that none of the programs a compiler successfully compiles will contain type errors.

Now, what is a type error? In principle, you can specify any undesirable property as a type error, and some type systems will be able to statically ensure no program has such an error.

By "property" above, I mean some type of logical proposition that applies to your program, for instance, "all indices are within array bounds". Other types of properties include, "all deferenced pointers are valid", "this program doesn't perform any I/O", or "this program performs I/O only to /dev/null", etc. Just about any sort of property can be specified and type checked in this way, depending on the expressiveness of your type system.

Dependent type systems are among the most general of type systems, via which you can enforce pretty much any property you like. It's not necessarily easy to do so though, as sophisticated properties are subject to incompleteness courtesy of Gödel.