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