What's the point of type safety? [closed]

Question

It has been advertised that in type-safe languages, well-typed programs never go wrong, but this doesn't like a legit statement to me:

1. Array indexing is usually by int, but we can freely send out of bound indices or even negative ones. In these cases we get exceptions if we're lucky or crash
2. Pointer arithmetic is purely chaotic in terms of "going wrong" yet they are type-safe if we disallow casting
3. Some program that wouldn't go wrong are not well-typed, like <"this is a string", (λx. "1" + 2)>.1 is not well-typed but the code in the second component of the tuple is unreachable hence no type error will occur at runtime

It is true that well-typed terms in STLC don't go wrong, but that's because STLC is total and normalizes and wow. Apparently, not all languages are STLC. What am I missing here? Is it actually meaningful to be type-safe?

Answer 1

well-typed programs never go wrong

“Go wrong” is an informal expression and you need to understand what it means in this context. It doesn't mean that programs written in type-safe languages don't have bugs. No type system is going to flag this code (in a fictional language) as wrong:

let add_one (x : int) = (x + 2) : {y:int | y = x + 2}

The specification contradicts the function name, but that's beyond the power of a type system, even one that can specify that the return value of the function has an arithmetic relationship with the argument.

A more precise statement would be that well-typed programs have well-defined behavior. Or, in other words, the semantics of well-typed languages does not include cases of undefined behavior.

The defined behavior can be to signal an error at runtime. The point of type safety is that you're guaranteed an error, as opposed to really bad effects such as arbitrarily corrupting memory. At one extreme, with a purely dynamic type system such as Lisp or Python, any program might suddenly stop with a runtime type error at any point. Languages with a static type system restrict the places where a runtime error can occur. The more expressive the type system is, the fewer places a runtime error can occur. Due to Rice's theorem, you can't have a nontrivial type system that both allows all computable functions and has no runtime errors.

Array indexing is usually by int, but we can freely send out of bound indices or even negative ones. In these cases we get exceptions if we're lucky or crash

You don't only get exceptions “if you're lucky”: getting an exception from an out-of-bounds array index is guaranteed. It's part of the semantics of the array indexing operator: a[i] returns the element at position i, or raises the IndexOutOfBounds exception of i is not a valid position. This is different from unsafe languages such as C¹ which cannot guarantee that a is an array and, even if it is, cannot keep track of its size.

Pointer arithmetic is purely chaotic in terms of "going wrong" yet they are type-safe if we disallow casting

Pointer arithmetic is array indexing seen from another angle. There are many language features other than casting that can break pointer arithmetic. For example, in C, void * conversion allows the programmer to lie freely about the type of a pointer.

Type-safe languages generally don't allow the programmer to build a pointer. You only have access to objects defined by the language.

Some program that wouldn't go wrong are not well-typed

That's true, but irrelevant. The claim is about well-typed programs. It doesn't say anything about programs that are not well-typed.

It is true that well-typed terms in STLC don't go wrong, but that's because STLC is total

Yes, “total” is one way to phrase progress.

and normalizes

No, normalization is irrelevant. STLC plus a recursion combinator is still type-safe.

and wow

I have no idea what this is supposed to mean.

¹ _{C as specified in theory or C as implemented in practice. It's theoretically possible to make a C implementation that detects all runtime errors, but it would be extremely inefficient.}

Answer 2

The wikipedia article on type safety expands upon your "don't go wrong" characterization:

Intuitively, type soundness is captured by Robin Milner's pithy statement that well-typed programs cannot "go wrong". In other words, if a type system is sound, then expressions accepted by that type system must evaluate to a value of the appropriate type (rather than produce a value of some other, unrelated type or crash with a type error).

My emphasis on "with a type error".

This is not the statement that a well-typed program never crashes, and certainly is not the much stronger statement that a well-typed program always terminates with a correct output.

With that in mind we can evaluate type safety in the context of your examples.

In the first example, in a type-safe language the guarantee provided is not "indexing always succeeds". It is that when doing x[i] when x is T, if i is in bounds, then the result is a variable of type T".

In the second example, in a type-safe language the guarantee provided is not "dereferencing a pointer never crashes". It is that when doing*(x+i) on x of type T* if the preconditions of correct pointer arithmetic are met -- that is, the resulting pointer is still inside the bounds of the thing x pointed to -- then dereferencing the pointer produces a variable of type T.

I don't understand the third example.

Note also that type safety is a matter of degree. Is C# a type-safe language? To a degree! There are many ways in which C# is unsound so in an absolute sense it is not type-safe, but a foundational design principle is that a great many common type errors must be flagged at compile time.

What's the point of type safety?

Primarily, to improve both developer productivity and program correctness by identifying a large class of defects at compile time.

A secondary benefit of type safety is that an optimizer which knows that certain type safety conditions are met can often generate more efficient code. And of course the converse is also true: type-unsafe languages might need to slow down.

My favourite example of the latter going wrong can be found in C# and Java. One of the unsoundnesses I mentioned before is type-unsafe array covariance:

Animal[] animals = new Giraffe[10]; // Weird but legal
animals[1] = new Tiger(); // Runtime type error!

Since the type system is unsound, it does not prevent the unsafe assignment. Thus the generated code must do a runtime check on the second line to verify that a Tiger can go into this particular array of Animals.

The common case -- the array really is Animal[] as it says on the tin -- gets slower as a result of this unsoundness.

Answer 3

Type safety is another layer of bug prevention.

A type unsafe language would let you freely and without any diagnostic message and without conversion (think the auto int to float conversion in many languages) reinterpret any value like another type.

This is what you can do in assembly, everything in assembly is a register-sized value and there is no barrier to interpreting the bits of a float like an integer.

But historically we moved away from the raw assembly model very quickly.

Adding types means that the compiler can catch simple errors like forgetting to make a number constant a floating point value. It also allows for shorthands when dealing with pointers to structures instead of manually computing the offset of a field every time you want to access it.

Doing things like automatic bounds checking is another layer that will need to build on top of basic types. How can you check bounds of an array when you don't have an array with a length you can access?