Difference between statically and dynamically typed languages

Question

When writing a course on computer science where students get an introduction to both Python and OCaml, I was on the verge of saying that Python is dynamically typed and OCaml is statically typed. I imagine that we all agree this is true even if nobody seems to agree on what exactly is a dynamically typed language. I came across several definitions which don't suit me :

• Some of them talks about type errors detection at compile time and at run time. As C can be compiled but also interpreted (well, this is very unusual, but it can be), I don't like this definition as it relies much more on the implementation of a language rather than on its semantics.

• Some ask that types should be attached to variables and not to values for a type system to be static. For instance, in C one can assign an int to a given variable : int n =1. But one cannot assign a double to this variable later. That would make the C language statically typed (well it is, but for other reasons). I don't like this definition as it seems it would not be too difficult to turn any statically typed language into a dynamic one.

• Many other definition which turned out to be wrong

I now believe that static/dynamic typed languages are not correctly defined as most serious books seems to be reluctant to define it. In "Types and programming languages" by B. Pierce, the author seems to imply that a language that can write:

if cond then 1 else "one"

should be dynamically typed. I've also seen the definition: "A statically typed language is a language where expression have types, whereas a dynamically typed language is one where values have a type". I am not quite sure to understand what it means. But my feeling is the following : a static language is a language where we can infer the type of an expression from the types of all its functions and its values. That would be a language where only functions whose output type is known from its input types are allowed. Julia people call it "type stable functions".

So my question is the following: Are statically typed languages, those who only allow "type stable functions"?

Answer 1

The question is subtle and simple at the same time, hence deep. Let me give you a simplifying answer.

First you need to realise there there three somewhat orthogonal distinctions which are often mixed up, leading to confusion:

• Typed vs untyped languages
• Type-checking vs type-inference
• Static vs dynamic typing

Types are simply an algorithmic technique to define and decide language subsets (think: if a program is typable, it's in the subset). Typically subset decided by types are somehow well-behaved, and we consider programs not in the subset to be somehow bad or in error, think programs like "hello" * 17 are rejected). The essence of this algorithmic technique is that you have a second language (that of types) which gives a second version on the program in question. Typically the language of types is simpler than the ambient programming language.

Type-checking vs type-inference is about a detail of this algorithmic technique: in type-checking a program is compared against user-specified types: are the two in 'harmony', while in type-inference the internal consistency of a program with itself is checked. In practise no programming language is fully type-checked, instead at least some parts of programs are inferred, e.g. you don't have to write

((3 : int) (+ : (int, int) -> int) (4 : int)) : int

or some monstrosity like this, instead, you can get away with

3 + 4

even in Java.

Finally statically vs dynamically typed is about when programs are accepted or rejected. With dynamic typing that happens during execution. With static typing, there is a distinct phase (sometime called semantic analysis) before execution, typically during compilation. If the program fails semantic analysis, compilation or interpretation is abandoned, hence no execution.