Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

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?

share|improve this question

migrated from stackoverflow.com Oct 24 '13 at 17:51

This question came from our site for professional and enthusiast programmers.

    
I'm not certain that type systems provide any benefit for non-compiled language, but as a long term user of compiled languages, I find that compiled languages with careful type checking are effective in preventing many kinds of ambiguous, undefined or incomplete code from getting past the "compile" stage. I guess you could say that type hints and a Lint system are valuable for Web Scripting (JavaScript) and if so, I'm sure we'll see enough of them. Dart anyone? Dynamic languages like Python seem no worse for the lack of a static type system. –  Warren P Oct 25 '13 at 0:40
1  
Today we understand that typing should be behavioral and not structural. Sadly, most modern programming languages have no way to assert the behavior of a type (see this question for a nice read). This makes the type system pretty useless in most cases especially since simple type errors that answers mention here can be caught by a clever linter that checks for common issues. –  Benjamin Gruenbaum Oct 25 '13 at 1:56
2  
@BenjaminGruenbaum What your describing already exists in languages like OCaml statically. It's called structural typing, it's actually quite old, nominal typing is newer. –  jozefg Oct 25 '13 at 2:41
1  
@BenjaminGruenbaum: ...What!? It is obviously not undecidable in statically-typed languages, or else writing a compiler for those languages would be impossible. –  BlueRaja - Danny Pflughoeft Oct 25 '13 at 17:27
4  
@BenjaminGruenbaum: Your comments are valuable, and that paper is interesting, but it does not bear out your claim that "it's usually undecidable in static languages like Java too", since it demonstrates that it is decidable in C#, and leaves open the question of whether it's undecidable in Java. (And anyway, IME, when a compiler for a statically-typed language can't decide that something is well-typed, it rejects it (or fails to compile it), so undecidability is an annoyance rather than a hole in the type-safety.) –  ruakh Oct 26 '13 at 22:55
show 4 more comments

8 Answers

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.

share|improve this answer
19  
+1 for compiling as the equivalent to writing a lot of tests. –  Dan Neely Oct 24 '13 at 19:10
2  
@DanNeely It's merely to illustrate that in a dynamic language, you need to exercise all parts of the code to catch the errors which a type system checks for free. And in a dependently typed language, you actually can entirely replace tests with types. Many times you need to prove additional theorems of correctness though –  jozefg Oct 24 '13 at 19:14
3  
If your type system has proved that your program must terminate, it's (probably) done so by proving that it is computing a primitive-recursive function. Which is cool I suppose, but a significantly less interesting complexity class than that which a true Turing Machine can solve. (It doesn't mean that the intermediate values aren't large; the Ackermann function is primitive-recursive…) –  Donal Fellows Oct 24 '13 at 21:21
4  
@DonalFellows The Ackermann function isn't primitive recursive, although it is a total computable function. –  Taymon Oct 25 '13 at 0:59
3  
@sacundim Exactly, languages like agda allow for optional totality checking and in the rare cases where you do want arbitrary recursion you can ask nicely, it's quite a slick system. –  jozefg Oct 25 '13 at 2:37
show 18 more comments

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.

share|improve this answer
4  
And a clever linter in an IDE like WebStorm JavaScript can say "Possible undefined reference to a.length for number a". This is not given to us by having an explicit type system. –  Benjamin Gruenbaum Oct 25 '13 at 1:58
4  
1. Statically not strongly 2. @BenjaminGruenbaum Yes, but this is done by chasing a graph of assignments in the background, think of it like a mini interpreter trying to figure out where things are going. Much harder than when types give you it for free –  jozefg Oct 25 '13 at 2:33
4  
@BenjaminGruenbaum: Don't confuse implicit/explicit with strong/weak. Haskell, for example, has an incredibly strong type system that puts most other languages to shame, but due to certain language design decisions made it's also capable of almost entirely universal type inference, essentially making it a strongly implicit typed language with support for explicit typing (That you should use, because the type inferencer can only deduce from what you wrote, not what you meant!) –  Phoshi Oct 25 '13 at 8:14
6  
“strongly-typed language will force you to explicitly state that a is an array” That’s wrong. Python is strongly typed and doesn’t require that. Even statically-and-strongly typed languages don’t require that if they support type inference (and most mainstream languages nowadays do, at least partly). –  Konrad Rudolph Oct 25 '13 at 10:00
    
@Phoshi That's not what I meant at all, by "explicit" type system I didn't mean you have to type everything - most modern languages like Scala or C# have type inference. I meant typing is explicit at the language level (not the actual code typed) –  Benjamin Gruenbaum Oct 25 '13 at 18:01
show 2 more comments

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.

share|improve this answer
    
+1 for simplicity. –  evilcandybag Oct 25 '13 at 15:43
add comment

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

Type safety is a property of a program brought by a sound type system and informed by a respective type checker (usually performed by a compiler). In very few words, a type safe program can be defined as one that, when executed, is guaranteed to not raise any type errors (e.g., every operation written in the program is defined for the operand types, etc).

In this sense, casting can be an unsafe operation:

Bar b = make_bar();
Foo f = (Foo) b;
do_something_with_foo(f); // might fail

What are the safety benefits of a type system?

In a single sentence: cost-effective checking for an entire class of errors (type errors) upfront, during compilation.

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

I would say having the descriptions of types for all values used and type information of operations performed in the program, which makes it amenable to analysis and check for validity. For more details, I suggest Cardelli's excelent introduction to the subject: Type Systems

share|improve this answer
1  
+1 for the paper, I'll have to start linking to that –  jozefg Oct 25 '13 at 2:43
add comment

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.

share|improve this answer
    
This sells dynamic typing short, failing to mention its primary benefits (the ones mentioned are handy by relatively unimportant). It also seems to imply something strange about unit tests -- yes, they're hard to do and have a cost, and that applies to statically-typed languages as well. What is this trying to say? It also fails to mention the limitations (by design) of current type systems, both in what they can express and in what errors they can catch. –  Matt Fenwick Dec 12 '13 at 10:46
    
@MattFenwick what do you feel are the primary benefits of dynamic typing? –  GlenPeterson Dec 12 '13 at 16:00
    
Typical static type systems reject many well-typed programs by design. (an alternative) (BTW, my criticism was only directed at the 3rd and 4th paragraphs.) –  Matt Fenwick Dec 19 '13 at 16:40
add comment

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.

share|improve this answer
2  
I object to "strongly typed". You mean statically typed. Strongly type carries pretty much no meaning, it's used to basically say "I like this type system" –  jozefg Oct 24 '13 at 19:21
    
@ jozefg Good point. I will amend the post. –  AsymLabs Oct 24 '13 at 19:24
3  
It is also not useful to say interpreted language... about a language implementation yes, but not the language itself. Any language can be interpreted or compiled. And even after the edit you are using the terms strong and weak typing. –  Esailija Oct 24 '13 at 20:24
3  
@jozefg: I always thought that strongly typed meant that each value has a fixed type (e.g. integer, string, etc), whereas weakly typed means that a value can be coerced to a value of another type, if it is considered convenient to do so. E.g., in Python (strongly typed), 1 + "1" throws an exception, whereas in PHP (weakly typed) 1 + "1" produces 2 (string "1" is automatically converted to integer 1). –  Giorgio Oct 24 '13 at 21:06
1  
@Giorgio with such definition for example Java is not strongly typed. But in many cases it is claimed to be. There is just no meaning to these words. Strong/Weak typed have much more accurate definition as "I like/don't this language" like jozefg says. –  Esailija Oct 24 '13 at 22:04
show 5 more comments

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.

share|improve this answer
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.