> Those type hints are not used at runtime for performance.

This is not a requirement for a language to be statically typed. Static typing is about catching type errors before the code is run.

> Type hint a var as a string then set it to an int, that code still gonna try to execute.

But it will fail type checking, no?

The critique is that "static typing" is not really the right term to use, even if preceded by "optional". "Type hinting" or "gradual typing" maybe.

In static typing the types of variables don't change during execution.

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.

'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.

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

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?

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.

That’s not really “the definition”. Different type systems can express different properties about objects, and there are absolutely cases that something changes about a type.

E.g. in structural typing, adding a new field will change the type to a subtype. Will it make any structural typed language non-static?