> In Python I can get a lot done and really don't miss types at all
No wonder, because Python has types (well … most everything does; but Python isn’t unityped [1]). It’s even relatively strongly typed. It’s just not statically typed (what the video calls “typed”).
That said, I do miss static type checking in Python, and a lot of the tooling and methodology around Python (pylint, TDD…) are a direct consequence of that lack of static checking.
— You seem to be aware of this but the distinction between “has types” and “has static typing” is actually fairly important. APIs in general often take advantage of Python’s extensible type system.
Read the article again. He says Python is unityped. The word "type" in mathematics and computer science has a meaning which is not the same as your usage of the word.
Well-typed programs should not go wrong. Python programs can crash at runtime due to simple type errors (expected integer but got a string). A crash is a crash, from a theoretical point of view it matters not that the error is prettier than a segmentation fault. Python is not strongly typed, it just has good error messages.
Blah you’re right. That’s quite a serious oversight on my part, it’s been too long since I’ve read that article and I had apparently forgotten its core idea.
Robert Harper is saying the exact opposite of what you’re quoting him to say. He would 100% call Python unityped (at least prior to the new type annotations, and probably even with them).
> TDD…) are a direct consequence of that lack of static checking.
Static checking gives you basic unit testing. TDD is far more expansive than unit testing. Static checking is not going to integration test your app for you.
The things in Python you call types are traditionally referred to as tags. Tagged values are values of one type (the type in Python) but which can still be distinguished based on a run-time check of their tag.
Python only has one type. To quote from the article by professor Harper:
"And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer."
Moreover, a tag is an implementation detail which rarely represents everything about a type.
E.g. a tag might tell us that some object is a function. But to know how many arguments it has, whether some are optional, and so on, we have to inspect fields beyond the tag.
No wonder, because Python has types (well … most everything does; but Python isn’t unityped [1]). It’s even relatively strongly typed. It’s just not statically typed (what the video calls “typed”).
That said, I do miss static type checking in Python, and a lot of the tooling and methodology around Python (pylint, TDD…) are a direct consequence of that lack of static checking.
— You seem to be aware of this but the distinction between “has types” and “has static typing” is actually fairly important. APIs in general often take advantage of Python’s extensible type system.
[1] See e.g. https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...