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

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

<ul>
<li>Typed vs untyped languages  </li>
<li>Type-checking vs type-inference </li>
<li>Static vs dynamic typing</li>
</ul>

<p>Types are simply an <em>algorithmic technique</em> 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 <code>"hello" * 17</code> are rejected).
The essence of this algorithmic technique is that you have a <em>second</em> 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.</p>

<p>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</p>

<pre><code>((3 : int) (+ : (int, int) -&gt; int) (4 : int)) : int
</code></pre>

<p>or some monstrosity like this, instead,
you can get away with</p>

<pre><code>3 + 4
</code></pre>

<p>even in Java. </p>

<p>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. </p>

CC BY-SA 4.0
2019-06-02T09:49:05.457Z
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
CC BY-SA 4.0
2019-06-02T10:42:34.203Z
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
CC BY-SA 4.0
2019-06-01T21:34:22.807Z
2019-06-01T21:58:36.177Z
2019-06-01T21:58:36.177Z
Martin Berger
<p>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 :</p>

<ul>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>Many other definition which turned out to be wrong</p></li>
</ul>

<p>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:</p>

<p>if cond then 1 else "one"</p>

<p>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".</p>

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

CC BY-SA 4.0
2019-06-01T16:25:32.733Z
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
CC BY-SA 4.0
2019-06-01T16:29:18.390Z
Is this a *theoretical* computer science class, or a software engineering class?
Robert Harvey
CC BY-SA 4.0
2019-06-01T16:33:57.847Z
Alright.  I'm going to migrate your question to Theoretical Computer Science.  Stand by while I pull the levers.  *[whooshing sound]*
Robert Harvey
<type-systems>
Difference between statically and dynamically typed languages
InsideLoop
# Difference between statically and dynamically typed languages

(Asked by: username_0 on 2019-06-01)

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

**Tags:** type-systems

> **Comments:**
> **username_1**: 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.*  
> **username_1**: Is this a *theoretical* computer science class, or a software engineering class?  
> **username_1**: Alright.  I'm going to migrate your question to Theoretical Computer Science.  Stand by while I pull the levers.  *[whooshing sound]*  

---

## 1 answers

### Answer by username_2 on 2019-06-01. Score: 2

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.

> **Comments:**
> **username_0**: 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.  
> **username_2**: 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.  

---

