[Python-ideas] Structural type checking for PEP 484

[Andrew Barnert]

On Sep 16, 2015, at 13:57, Sven R. Kunze <srkunze at mail.de> wrote:

> Sometimes and sometimes that. That can't be right for something to basic like types.

Types aren't as basic as you think, and assuming they are leads you to design languages like Java, that restrict you to working within unnecessary constraints. For an obvious example, what's the return type of json.loads (or, worse, eval)?

Haskell, Dependent ML, and other languages have made great strides in working out how to get most of the power of a language like Python (and some things Python can't do, too) in a type-driven paradigm, but there's still plenty of research to go. And, even if that were a solved problem, nobody wants to rewrite Python as an ML dialect, and nobody would use it if you did.

Python solves the json.loads problem by saying its runtime type is defined lazily and implicitly by the data. And there's no way any static type checker can possibly infer that type. A good statically-typed language can make it a lot easier to handle than a bad one like Java, but it will be very different from Python.

> Couldn't these problems not be solved by further research on typecheckers?

I'm not sure which problems you want solved.

If you want every type to be inferable, for a language with a sufficiently powerful type system, that's provably equivalent to the halting problem, so it's not going to happen.

More importantly, we already have languages with a powerful static type system and a great inference engine, and experience with those languages shows that it's often useful to annotate some types for readability that the inference engine could have figured out. If a particular function is more understandable to the reader when it declared its parameter types, I can't imagine what research anyone would do that would cause me to stop wanting to declaring those types.

Also, even when you want to rely on inference, you still want the types to have meaningful names that you can read, and could have figured out how to construct on your own, for things like error messages, debuggers, and reflective code. So, the work that Jukka is proposing would still be worth doing even if we had perfect inference.

> Btw. I can tell the same anecdote when switching from C/C++/C#/Java to Python. It was like a liberation---no explicit type declarations anymore. I was baffled and frightened the first week using it. But I love it now and I don't want to give that freedom up. Maybe, that's why I am reluctant to use it in production.

The problem here is that you're coming from C++/C#/Java, which are terrible examples of static typing. Disliking static typing because of Java is like disliking dynamic typing because of Tcl. I won't get into details of why they're so bad, but: if you don't have the time to learn you a Haskell for great good, you can probably at least pick up Boo in an hour or so, to at least see what static typing is like with inference by default and annotations only when needed in a very pythonesque languages, and that will give you half the answer.