Type Systems – What Are the Safety Benefits of a Type System

type-safetytype-systems

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?

Best Answer

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

Out-of-range errors
SQL injection
Generalizing 2, many safety issues (what taint checking is for in Perl)
Out-of-sequence errors (forgetting to call init)
Forcing a subset of values to be used (for example, only integers greater than 0)
~~Nefarious kittens~~ (Yes, it was a joke)
Loss-of-precision errors
Software transactional memory (STM) errors (this needs purity, which also requires types)
Generalizing 8, controlling side effects
Invariants over data structures (is a binary tree balanced?)
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.

Related Solutions

Type Systems – When Is Type Testing OK?

"Never" is the canonical answer to "when is type testing okay?" There's no way to prove or disprove this; it is part of a system of beliefs about what makes "good design" or "good object-oriented design." It's also hokum.

To be sure, if you have an integrated set of classes and also more than one or two functions that need that kind of direct type testing, you're probably DOING IT WRONG. What you really need is a method that's implemented differently in SuperType and its subtypes. This is part and parcel of object-oriented programming, and the whole reason classes and inheritance exist.

In this case, explicitly type-testing is wrong not because type testing is inherently wrong, but because the language already has a clean, extensible, idiomatic way of accomplishing type discrimination, and you didn't use it. Instead, you fell back to a primitive, fragile, non-extensible idiom.

Solution: Use the idiom. As you suggested, add a method to each of the classes, then let standard inheritance and method-selection algorithms determine which case applies. Or if you can't change the base types, subclass and add your method there.

So much for the conventional wisdom, and on to some answers. Some cases where explicit type testing makes sense:

It's a one-off. If you had a lot of type discrimination to do, you might extend the types, or subclass. But you don't. You have just one or two places where you need explicit testing, so it's not worth your while to go back and work through the class hierarchy to add the functions as methods. Or it's not worth the practical effort to add the kind of generality, testing, design reviews, documentation, or other attributes of the base classes for such a simple, limited usage. In that case, adding a function that does direct testing is rational.
You can't adjust the classes. You think about subclassing--but you can't. Many classes in Java, for instance, are designated final. You try to throw in a public class ExtendedSubTypeA extends SubTypeA {...} and the compiler tells you, in no uncertain terms, that what you're doing is not possible. Sorry, grace and sophistication of the object oriented model! Someone decided you can't extend their types! Unfortunately, many of the standard library are final, and making classes final is common design guidance. A function end-run is what's left available to you.

BTW, this isn't limited to statically typed languages. Dynamic language Python has a number of base classes that, under the covers implemented in C, cannot really be modified. Like Java, that includes most of the standard types.
Your code is external. You are developing with classes and objects that come from a range of database servers, middleware engines, and other codebases you can't control or adjust. Your code is just a lowly consumer of objects generated elsewhere. Even if you could subclass SuperType, you're not going to be able to get those libraries on which you depend to generate objects in your subclasses. They're going to hand you instances of the types they know, not your variants. This isn't always the case...sometimes they are built for flexibility, and they dynamically instantiate instances of classes that you feed them. Or they provide a mechanism to register the subclasses you want their factories to construct. XML parsers seem particularly good at providing such entry points; see e.g. a JAXB example in Java or lxml in Python. But most code bases do not provide such extensions. They're going to hand you back the classes they were built with and know about. It generally will not make sense to proxy their results into your custom results just so you can use a purely object-oriented type selector. If you're going to do type discrimination, you're going to have to do it relatively crudely. Your type testing code then looks quite appropriate.
Poor person's generics/multiple dispatch. You want to accept a variety of different types to your code, and feel that having an array of very type-specific methods isn't graceful. public void add(Object x) seems logical, but not an array of addByte, addShort, addInt, addLong, addFloat, addDouble, addBoolean, addChar, and addString variants (to name a few). Having functions or methods that take a high super-type and then determine what to do on a type-by-type basis--they're not going to win you the Purity Award at the annual Booch-Liskov Design Symposium, but dropping the Hungarian naming will give you a simpler API. In a sense, your is-a or is-instance-of testing is simulating generic or multi-dispatch in a language context that doesn't natively support it.

Built-in language support for both generics and duck typing reduce the need for type checking by making "do something graceful and appropriate" more likely. The multiple dispatch / interface selection seen in languages like Julia and Go similarly replace direct type testing with built-in mechanisms for type-based selection of "what to do." But not all languages support these. Java e.g. is generally single-dispatch, and its idioms are not super-friendly to duck typing.

But even with all these type discrimination features--inheritance, generics, duck typing, and multiple-dispatch--it's sometimes just convenient to have a single, consolidated routine that makes the fact that you are doing something based on the type of the object clear and immediate. In metaprogramming I have found it essentially unavoidable. Whether falling back to direct type inquires constitutes "pragmatism in action" or "dirty coding" will depend on your design philosophy and beliefs.

Functional Programming – Alternatives to Language Purity

You have described an effect system. It’s true that there are other effect systems than monads, but in practice monads give you a lot of expressive power that you would need to reinvent in any practical effect system you might devise.

For example:

I start by tagging my I/O procedures with an io effect.
My pure functions can still throw exceptions, but throwing exceptions isn’t io, so I add an exn effect. Now I need to be able to combine effects.
I want to have non-I/O functions that use mutation internally on a local heap h, and I want the compiler to make sure that my mutable references don’t escape their scope, so I add an st<h> effect. Now I need parameterised effects.
For higher-order functions, I need to write multiple versions for every combination of effects I want to support—for example, map with a pure function versus map with an impure function. Now I need effect polymorphism.
I notice that my user-defined type could be used to model effects (benign failure, nondeterminism) that the language doesn’t have natively. Now I need user-defined effects.

Monads support all of these use cases:

Functions that may return errors can use the Either monad.
Effects can be combined with monad transformers—if I need exceptions and I/O, I can use the EitherT IO monad.
Monads can be parameterised like any other type; the ST h monad lets you do local mutation on STRefs in the scope of a heap h.
Because of the Monad typeclass, I can overload an operation to work on any kind of effect. For example, mapM :: (Monad m) => (a -> m b) -> [a] -> m [b] works in IO, but it also works in Either or ST or any other monad.
All monads are implemented as user-defined types, except for things like IO and ST which must be implemented in the Haskell runtime.

There are of course some significant warts in Haskell’s use of monads for side effects.

For one thing, monad transformers are generally not commutative, so StateT Maybe is different from MaybeT State, and you have to be careful to choose the combination that you actually mean.

The bigger problem is that a function can be polymorphic in which monad is being used, but it cannot be polymorphic in whether a monad is being used. So we get loads of duplicated code: map vs. mapM; zipWith vs. zipWithM, &c.

Now, in answer to your actual question…

Koka from Microsoft Research is a language with an effect system that does not suffer from these problems. For example, the type of Koka’s map function includes a type parameter e for effects:

map : (xs : list<a>, f : (a) -> e b) -> e list<b>

And this parameter can be instantiated to the null effect, making map work for pure and impure functions alike. In addition, the order in which effects are specified is immaterial: <exn,io> is the same as <io,exn>.

It’s also worth mentioning that Java’s checked exception mechanism is an example of an effect system that people have widely accepted, but I don’t feel it adequately answers your question because it’s not general.