[zarzavat]

If there’s any checking of types before program runs then it’s static typing. Gradual typing is a form of static typing that allows you to apply static types to only part of the code.

I’m not sure what you mean by variables not changing types during execution in statically typed languages. In many statically typed languages variables don’t exist at runtime, they get mapped to registers or stack operations. Variables only exist at runtime in languages that have interpreters.

Aside from that, many statically typed languages have a way to declare dynamically typed variables, e.g. the dynamic keyword in C#. Or they have a way to declare a variable of a top type e.g. Object and then downcast.

[neonsunset]

'dynamic' in C# is considered a design mistake and pretty much no codebase uses it.

On the other hand F# is much closer to the kind of gradual typing you are discussing.

[mondrian]

Python is dynamically typed because it type-checks at runtime, regardless of annotations or what mypy said.

[kaba0]

Is java dynamically typed as well, then? It does reify generics, so only some part is type checked, what is the level at which it is statically/dynamically typed?

[mondrian]

Yeah Java is partially dynamically typed. I think we can safely conclude that all practical languages are hybrids where some of the type checking is done by the compiler and some of the type checking is deferred to the runtime.

Then when we call a language statically typed we mean most of the type checking is usually done statically. Dynamic type checking is the exception, not the rule.

Even in dynamically typed languages like Python, some of the type checking may be done by an optimizer in the compilation stage. The runtime type check guarding some operations may be removed, because the optimizer decides it knows the types of the values involved once and for all.