Definition of statically typed and dynamically types

Question

Which of these two definitions is correct?

• Statically typed - Type matching is checked at compile time (and therefore can only be applied to compiled languages)
• Dynamically typed - Type matching is checked at run time, or not at all. (this term can be applied to compiled or interpreted languages)

---

• Statically typed - Types are assigned to variables, so that I would say 'x is of type int'.
• Dynamically typed - types are assigned to values (if at all), so that I would say 'x is holding an int'

By this definition, static or dynamic typing is not tied to compiled or interpreted languages.

Which is correct, or is neither one quite right?

Answer 1

Which is correct, or is neither one quite right?

The first pair of definitions are closer but not quite right.

Statically typed - Type matching is checked at compile time (and therefore can only be applied to compiled languages)

This is tricky. I think if a language were interpreted but did type checking before execution began then it would still be statically typed. The OCaml REPL is almost an example of this except it technically compiles (and type checks) source code into its own byte code and then interprets the byte code.

Dynamically typed - Type matching is checked at run time, or not at all.

Rather:

Dynamically typed - Type checking is done at run time.

Untyped - Type checking is not done.

Statically typed - Types are assigned to variables, so that I would say 'x is of type int'.

Dynamically typed - types are assigned to values (if at all), so that I would say 'x is holding an int'

Variables are irrelevant. Although you only see types explicitly in the source code of many statically typed languages at variable and function definitions all of the subexpressions also have static types. For example, "foo" + 3 is usually a static type error because you cannot add a string to an int but there is no variable involved.

Answer 2

One helpful way to look at the word static is this: static properties are those that hold for all possible executions of the program on all possible inputs. Then you can look at any given language or type system and consider which static properties can it verify, for example:

• JavaScript: no segfaults/memory errors

• Java/C#/F#: if a program compiled and a variable had a type T, then the variable only holds values of this type - in all executions. But, sadly, reference types also admit null as a value - the billion dollar mistake.

• ML has no null, making the above guarantee stronger

• Haskell can verify statements about side effects, for example a property such as "this program does not print anything on stdout"

• Coq also verifies termination - "this program terminates on all inputs"

How much do you want to verify, this depends on taste and the problem at hand. All magic (verification) comes at price.

If you have never ever seen ML before, do give it a try. At least give 5 minutes of attention to Yaron Minsky's talk. It can change your life as a programmer.

Answer 3

The second is a better definition in my eyes, assuming you're not looking for an explanation as to why or how things work.

Better again would be to say that

• Static typing gives variables an EXPLICIT type that CANNOT change
• Dynamic typing gives variables an IMPLICIT type that CAN change

Answer 4

I like the latter definition. Consider the type checking when casting from a base class to a derived class in object oriented languages like Java or C++ which fits the second definition and not the first. It's a compiled language with (optional) dynamic type checking.