Frankly, each of your three paragraphs seems unrelated to each other, so I'm still not sure what your argument is.

1) Not type checking at runtime is exactly what people mean by static typing, because the definition of static typing means the checks are done before execution.

2) This does not make it harder to optimize, on the contrary if they generated type assertions it would considerable slow things down on the boundary of typed and untyped code.

3) C++, Go, Rust, Haskell they are fully statically typed, the only difference is they support varying levels type-inference which means you don't need to "type out the type" but it's really orthogonal to the whole optional/static/dynamic typing issue.

C++ and Go don't have type inference. All they do is set the type of new variables to whatever they're first initialized to. Type inference means figuring out the types of variables from how they're used. The litmus test for type inference is inferring function argument types.

I'm sorry, but that's not the definition of type inference.

"Type inference refers to the automatic deduction of the data type of an expression in a programming language."

https://en.wikipedia.org/wiki/Type_inference

Which you'll notice C++ and Go, are listed as languages with type inference.

But you're right that they don't have as nearly as strong type inference as rust, which doesn't have as strong as haskell etc.

Rust and Haskell have very similar type inference. The only major difference is that Rust doesn't infer type signatures, but that's a design decision, not a power issue.

> "Type inference refers to the automatic deduction of the data type of an expression in a programming language."

Depending on how simple "deduction" can be, that arguably includes every language that includes expressions.

And if the deduction is required to include usage information, it quite arguably excludes C++/Go style "var": a variable declaration is not an expression.

Generally, that Wikipedia article doesn't seem very good - check the talk page.

True, C++ and Go don't have a real type inference engine. They just compute the result type of an expression and use that to create the type of a variable in an assignment. However, this handles enough of the common cases to be quite useful.

(When you have a real type inference engine, you spend a lot of time trying to figure out what it did, or why it didn't do something.)

Nobody forces you to use type inference. If you think a particular piece of code is too tricky to understand without explicit type annotations, by all means use explicit type signatures.

That being said, I have never encountered a program that was hard to understand because types were inferred rather than explicitly annotated. I use explicit type annotations in two situations:

(0) As a compile-time analogue of printf debugging. Not exactly a joyous thing.

(1) At module boundaries, to control what modules expose to each other.

If you don't call what C++ and Go do "type inference", would you call it "type deduction"?

It really doesn't matter what he calls it, as type inference has a well accepted definition that includes Go and C++. See: https://en.wikipedia.org/wiki/Type_inference

Perhaps the parent was trying to talk about "HM type inference" or something, but "type deduction" is also a fine name for a subset of type-inference, and perhaps more explicit for C++ and Go.

Type inference (not just Hindley-Milner) is divided in two logical phases:

(0) Generating a system of type equations, by recursively scanning the AST.

(1) Solving the system of equations. The nontrivial nature of this step is what makes type inference, well, inference.

In Go and C++'s case, the generated type equations come out already solved (that is, of the form `TypeVar = TypeExpr`), so there's nothing to infer!

Perhaps you'd be best up taking it up on wikipedia and primary sources, instead of arguing with random internet people when using their same definitions.

I don't think it deserves a special name. Would you use a special term for the fact you don't need to specify that the sum of two ints is an int?

I disagree. Naming things is useful. "Type deduction" says clearly what happens, and is still distinct enough from "type inference" which is a different, more sophisticated concept. I've seen the term "type deduction" used many times in the context of C++ and Rust.

Rust has actual type inference. It just happens to be a local affair. For example, you can create a vector, even an empty one, without explicitly specific its element type. But, somewhere in the current function, you have to provide information about the element type, say, by inserting elements into the vector, or by using an element in a way that constrains its type.

The ability to name things is useful, but there are far more things out there than we can come up with good names for, so we have to decide wisely what things we name and what things we don't. Something like C++'s `auto` doesn't need a name of its own. It's just unidirectionally propagating type information from child to parent nodes in the AST. This is something even FORTRAN (when its name was all caps) and ALGOL implementations did during normal type checking.

Sorry, what are you talking about? Python runtime still does its existing dynamic type checking. You can still get a TypeError at runtime if you try hard enough.

Mypy is not about optimising anything, it's about static correctness guarantees. If you're developing PyPy, type hints shouldn't be making your life any better or worse.

Lastly, the 'direction' you describe that everyone else seems to be taking, is the exact same direction mypy has taken. Type annotations are only required at the method/function level.

This is not correct (try returning a defaultdict). That is the reason that Python 3.6 added a new inline type hint syntax

    My_dict: defaultdict[int, List[int]] = defaultdict(int)

Enforcing type hints would be impossible to implement without breaking a lot of existing Python code. If module A suddenly introduces them, module B that depends on it would have to suddenly make sure that all arguments it passes conform. If another module C depends on B and passes arguments that are in turn passed to module A, that basically means that the author of B is forced to add type hints to its code as well. In practice this would rapidly turn the whole language into a semi-statically typed one which (a) was never the intention and (b) would turn the whole ecosystem into a complete mess with incompatible typed and non-typed code unable to interact with each other.

If you add type hints to a function and it detects an error because it's called with the wrong type, it probably didn't work anyway.

I've run into that with functions that take NumPy arrays. You can pass a Python array, but "+" behaves very differently. For a NumPy array, it's element by element addition. For a Python array, it's concatenation. You want to catch that.

>It feels like Von Rossum is making life hard for the PyPy compiler project again.

Or perhaps, he realizes that to require these typechecks at runtime would either

- require a massive rewrite of the CPython interpreter

- cause a performance penalty in code that is statically typed (there are pure python libraries that allow this, and yes your code runs slower)

Further, it offers a relatively narrow amount of help to pypy, which has already come out and said that they have no interest in using annotations for efficiency gains, because they're a jit and they don't need them.

PyPy is written in RPython, which is Python with type annotations strict enough to allow hard precompilation to C. The type syntax is completely different from this new thing.[1] Only the built-in types are fully defined. There's "anytype", "sequence", and "object" to cover more general types without giving full details. This allows hard compilation of the stuff that compiles down to machine code, while dealing with user-defined object types more dynamically. That's one approach to typing Python.

Von Rossum on PyPy (2016): "Otherwise, there are specialized versions of Python like PyPy that are still around."

[1] https://bitbucket.org/pypy/pypy/src/default/rpython/translat...

I don't think there's anything preventing a future version of Python from implementing an optional command line flag to enforce declared types at runtime. And maybe the breaking change that results in a Python 4 will be enabling that option by default.

I hope so. I would love to have strict type annotation in development.

It's really strange to compare Python to C++, Go, and Rust, given that all the latter are statically typed languages with some amount of type inference, while Python is dynamically typed. A more appropriate comparison would be to something like JavaScript, where TypeScript and Flow both implement the same exact approach - optional type annotations that are checked at compile time and not enforced at runtime. Experience in the JS ecosystem has shown that it is a very successful approach.

Well in the pypy case, couldn't this just be a toggle? As in, you as the user guarantee that your type annotations are correct and strict, and if it isn't, then pypy will just blow up in your face when type annotations aren't respected.

I think that's a fair trade off, and easily doable. Those who want it and respect it get the speedup, those who don't don't lose anything.

I assure you, it's not that simple. You either check types at runtime (big performance penalty, aka: C Python) or you don't because a compiler (or JIT) did the leg work.

If you have to double check types at runtime, you've already lost.

But that's why I say, there should be a pypy flag where you tell it to not double check at run time and that you've made sure your annotation is correct.

Now if it isn't correct, you'll probably get a segfault or some nasty error and it'll blow up.