# Difference between statically and dynamically typed languages

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"?

• I am a teacher of both C and Java, and I find that wringing hands over word definitions like this is not productive. Here is a workable definition: a statically typed language can detect type errors at compile time. – Robert Harvey Jun 1 '19 at 16:25
• Is this a theoretical computer science class, or a software engineering class? – Robert Harvey Jun 1 '19 at 16:29
• I'm voting to close this question as off-topic because it belongs on cs.stackexchange.com. SO is for practical programming problems. – glennsl Jun 1 '19 at 16:31
• @Robert. Unfortunately, they learn OCaml which is statically typed. Although OCaml programs can be compiled, they never do it and only use a REPL. Therefore they use a statically-typed language which is not really "compiled". – InsideLoop Jun 1 '19 at 16:31
• @Robert. It is in France where things get theoritical very early. Let's say that a Turing-complete machine is introduced in the same course ! – InsideLoop Jun 1 '19 at 16:33

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.

• Thanks for your answer. Unfortunately, the definition you give is very implementation dependent. I imagine that a C compiler can avoid type checking and emits assembly code that checks types at runtime. That would make static/dynamic typing a property of the implementation, not of the language. But maybe it is. – InsideLoop Jun 2 '19 at 9:49
• Of course this is implementation dependent. C dynamically typechecked can run a larger set of programs than for example the C11 that clang or gcc accept. So they are strictly speaking two languages, but with similar surface syntax. – Martin Berger Jun 2 '19 at 10:42