and this one last year: https://www.youtube.com/watch?v=ST33zDM9vOE&t=68s
and finally this one in 2021: https://www.youtube.com/watch?v=Lj_9TyT3V98
I think I'll finally start using type checking - it really seems to just eliminate a whole class of potential bugs; a class that is often not tested at that.
As they are hints it means you can still pass in wrong values in some situations and what types check on one implementation may not type check with the other implementation. So the types are superficial only in Python.
The paper “Python 3 types in the wild” at https://news.ycombinator.com/item?id=26788177 is a good read. I enjoyed reading it and found it useful.
I’m a fan of types as the compiler tells me I made a mistake and blocks me making mistakes. You can use the type system to make certain errors unrepeatable (impossible to make). With that my preference is use a language where types are first class rather than a language trying to retrofit some loose form of type checking on top which is nothing more than linting.
Being a fan of strongly typed languages I was eager to use types in Python when I had to involuntarily use Python. After a few instances of putting in type hints and things type checking when they shouldn’t I mainly don’t bother with them now outside of data classes as they where not catching bugs I wanted so still getting runtime errors.
Could you elaborate. When can you pass in wrong values?
The type checkers aren't always precisely the same (some do inference, mypy doesn't), but the cases where they disagree are usually because one is correct and one wants more information, not because you're able to do the wrong thing despite having annotations.
I use it whenever I can and it helped me find many bugs in the code (especially not checking if value is None through the Optional). It also makes refactoring your code in IDEs that understand types (like PyCharm) much much easier.
Haskell types aren't checked at runtime either, so that can't be it.
Python has runtime type checks that do happen at runtime, so maybe it's Haskell that doesn't have types.
Python is dynamically typed. That means everything including things like string or integer is stored as a structure with a type. The checking of the type happens at runtime. This is major reason why languages like Python are so much slower than statically typed languages.
The annotated type in Python is providing mechanism of figuring out types before code is run, this helps finding bugs, but these types are not used during normal operation[1], but that doesn't stop them from being useful for finding bugs in the code or helping with refactoring.
[1] There are some packages that implement some runtime checks, but they IMO are waste of time. Basically they are ensuring that type problems that tool like mypy would detect also will cause your code to crash. It also add performance penalty as well.
There's also mypyc, code that compiles python code that using types increasing its performance. It is currently used to compile mypy increasing its performance by a factor of 4 I believe. It also makes some python features unavailable if you want to use it (https://mypyc.readthedocs.io/en/latest/differences_from_pyth...)
Mypy checks the type before runtime, just like GHC does.
Python also checks during runtime, but Haskell doesn't have that feature. Right?
> This is major reason why languages like Python are so much slower than statically typed languages.
Julia's dynamic typing, and hence its ability to do specialization using runtime information, is part of why it can (sometimes) beat Fortran in numerical performance.
I don't know Haskell so can't answer that, but typically a statically typed language doesn't need that.
Sometimes languages still provide runtime check, typically happens when their type system is lacking. For example in Go, if you use interface{} type, the type checking happens at runtime. That's why it is discouraged to use, because could be reason that slows down your code.
> Julia's dynamic typing, and hence its ability to do specialization using runtime information, is part of why it can (sometimes) beat Fortran in numerical performance.
I'm also not familiar with Julia, but from what I read is that for numerical types, Julia uses native types instead of using objects like Python.
It looks like well written Julia code can enable the interpreter to infer types and then JIT can use that to optimize the code. Python doesn't have that functionality at least not yet.
I don’t have the specific example, it was something I observed not so long ago, said well that’s shit, fixed my code issue and moved on. Not being a huge fan of Python outside of small scripts and only using Python as told to use Python I took little interest in the detail as was a case of just get the job done and move on.
It’s been a while since I read the paper I shared but think that mentions it something similar if I remember correctly.
Four: Mypy, Pyre, Pyright and Pytype.
Python has several type checkers, as does Haskell, each with different soundness properties. What makes GHC's type checking more "true" than Mypy's or Pytype's or Pyright's?
(There is also Liquid Haskell, but it doesn't check Haskell types, it checks Liquid Haskell types.)
GHC with its innumerable extensions and impenetrable (if well-defined) typing rules is and was always intended to be a testbed for wild type system ideas; that whatever it accepts became the received superset of standard Haskell (of which it is the only implementation) is in my opinion a failure of the Haskell community and the very thing that turned me away from Haskell after several years.
On the other hand, the only real description of what Mypy accepts is the source code of Mypy, and while many interesting programs that fall into that set also happen to be accepted by Pytype or whatever else, it’s not in any useful sense a bug if some are not. There’s also no practical way to tell if an arbitrary program is accepted except to try throwing it into the typechecker, because there is no human-adapted description of what constitutes being accepted.
None of which is to say that Mypy is not useful. It is useful, tremendously so. But as far as maturity of type systems in Haskell or SML goes, it’s not even in the same league. (So that this is not taken as academic elitism, neither are Scala, OCaml, or Typed Racket.)
The academic usage holds that the distinction between the true type systems and the pretenders is that the first are sound: a well-typed program either evaluates to a normal form (value) or fails to terminate, but can never get stuck (segfault, terminate with an uncaught exception, however your environment implements that).
Of course, a gradual system like Mypy can never both be sound in this sense and remain gradual (which is a major selling point for Mypy), so for them the rule is usually amended with “provided the program is fully annotated” (and it should be obvious whether any given program is fully annotated or not, otherwise the system is just user-hostile regardless of how sound it is; at the very least it must be decidable). That is still obviously not satisfied for Mypy, because it doesn’t track exceptions (and including uncaught exceptions in normal forms would be useless because then no Python programs would ever get stuck). The actual guarantee Mypy is supposed to provide sounds kind of wimpy, like “never gets a TypeError that is not explicitly raised in user code”, but would still be useful regardless... Except that soundness is usually a pretty non-trivial theorem, and the lack of a readable specification for Mypy’s type system precludes it from being proven.
While well-typed Haskell (or SML) programs can in fact crash from the user’s perspective, the possible sources of crashes are rare and avoidable enough (for Haskell, only non-exhaustive patterns and explicit use of undefined, error, or throw) that you can call them additional normal forms without making the whole thing trivial. Every other way an untyped program could get stuck is disallowed by the type system, and there is a proof (SML) or at least a proof sketch (Haskell) of that (although of course not every untyped program that can’t get stuck is allowed by the type system, that is impossible by Turing—Gödel). Even the horrendously complicated systems that GHC implements nowadays still have papers that prove their soundness for a good enough toy example that one walks away convinced that the real thing works just as well.
So yes, there is a sense in which Mypy’s system is less “true” than SML’s or Haskell’s, and it is directly caused by (though not completely reducible to) the lack of a complete human-readable spec for both Mypy and Python itself. (I love Python to bits, but its object model is surreal and its only complete description is Objects/object.c together with Objects/typeobject.c.) If a wizard waved his wand and made every copy of the Haskell Report disappear, its type system would technically remain sound, but illegibly so to human mathematicians, thus it would in fact become less “true” in this sense than previously. Multiple implementations help, but I expect that without a prose spec it wouldn’t be easy to tell that GHC, UHC and Hugs implement the same system, the same way I have no idea if Mypy and Pytype do.
It's hard to find people who are knowledgeable enough about both static and dynamic systems and able to explain in layman's terms. Is there somewhere (online?) I can go to talk with people like you?
The people on #haskell at Freenode (nowadays Libera) were extremely friendly and helpful when I frequented it about five to ten years ago, although of course there are a subtle but important limits to initiating discussions that are interesting to people on the channel but not strictly on topic for it.
My more general advice is (for a double combo of both trite and condescending) read a book. Specifically, read Pierce’s “Types and programming languages”. I usually cherry-pick paragraphs and sections from books rather than read them from start to finish, but this particular book I basically gulped down in two sittings on two-hour flights (being trapped in economy seating helps) and found extremely enlightening both in that it dissolved the mystery around some lofty-sounding words I was always afraid of (“corecursion” and “coinduction”, “terminating” vs “productive”) and in that it contained completely elementary mathematical insights that have previously passed me by (Tarski fixed point theorem and order theory in general).
While I did have an advantage of having encountered, if not understood, basically all of the words inside it beforehand, I still believe it might be helpful even if you have absolutely no background in type systems. And don’t be put off by the use of Java in the case study, it is genuinely on point there.
For a more practical and yet more advanced (dependent types!) view, you can try “Type-driven programming in Idris” and “The little typer”, but I haven’t studied the former as carefully and have only skimmed the latter, so can’t recommend either with the same degree of certainty. I guess just follow the general advice on difficult literature: look around, follow references, don’t hesitate to put down things that don’t work for you, and if all else fails, let it stew for a week before trying again.
GHC types are mathematically provable. Types are guaranteed to stay within your defnitions, so you can analyze the type graph without ever having to run the program.
Can you give an example of that? Mypy catches this:
def addsome(val: int) -> int:
val += 1.1 # tmp.py:2: error: Incompatible types in assignment (expression has type "float", variable has type "int")
return val
It's also static - does Mypy throw that error when that program is statically analysed, or at runtime?
You can certainly statically identify places where such changes are possible and the possible changes, in fact, Python static typecheckers do this.
> It's the Halting problem.
The Halting problem is a real thing, but you can simply bail out on any path that reaches a certain depth without resolution and fallback to the broadest possible type (failing narrower constraints) to avoid it.
Practically most large programs today can not pass maximal strictness settings as too many libraries lack type hints. But that's not a fundamental issue of python type system just a needed improvement of the ecosystem. Type hints are gradually growing and some major libraries have had noticeable improvements in the past year (numpy only started to have some types around 1.20).
It's also been my experience (C(++), Kotlin, Swift) that as the complexity of typing increases, 10% of the time I spend servicing types accounts for 90% of the sites I need typing, and the other 90% of the time spent on types is me cursing at the compiler trying to make it accept the odd 10%.
An optional type annotation system allows ME to pick where I want that effort/payback balance to be at on a case by case basis.
The project has now scaled to multiple developers and many thousands of lines of code. If I compare my experiences this time around with past experiences in Python, I feel those early choices are paying big dividends in terms of code readability and correctness.
In particular:
The ergonomics of data classes is great (IMO). They avoid a lot of boiler plate, integrate well with type checking and auto completion, and provide clear context to anyone reading the code.
I’ve found Mypy a bit flaky (sometimes it misses errors it seemingly should catch) and some things that cannot be expressed in the type system to be pain points but overall having type annotations present and enforced helps document code, works well with IDE auto completion, and occasionally picks up errors that would have been otherwise missed.
In particular I’ve found it’s picked up a lot of errors around missing None checks (nullability). These seem to be particularly easy to miss in unit tests.
I’ve also found that PyCharm’s built in code code checking has often been able to pick up and highlight problems which it would have otherwise missed thanks to having type annotations. Having early feedback on problems is nice productivity boost.
One hint if you do use Mypy make sure to enable check-untuned-defs. You’ll get much better coverage.
I think if you're a SWE or has a CS education or worked with a compiled language before, you know exactly what kind of problem typing is solving. For me, I have to first discover the problem, slowly learn that there is a solution out there, and finally realizing that my problem can be solved by this solution.
The formalization of problem space + the discovery of solutions + the final realization of matching solutions to problems are non-trivial. I'm a bit embarrassed that it took so long and a bit sad. But it is what it is.
It usually comes from people who never had experience with statically typed languages, don't work on projects with a large dev team, cross teams projects or work with a lot of 3rd party libraries. They don't realize the maintenance nightmare that types can easy.
Sure you write one off script, or something that is rarely run don't use types, but when you have a 50k lines codebase that is actively developed and maintained it's another story.
I'm so glad Typescript changed that mindset of frontend developers and is supported by a lot of prominent open source projects
Thinking that typing is good and buying that a pasted-on-after-the-fact typing system is good are different matters.
Change is always hard.
That’s not to say that typing isn’t useful - I use it daily, especially since VSC has made it a lot faster than mypy - but I do think the Python community is wide enough that you can find people legitimately saying it is or isn’t a big deal for them as a function of where they work. You also have a certain amount of PTSD from languages like Java which make typing far more labor intensive and through some combination of limited expressiveness, dynamic logic, and culture end up making the benefits less than anticipated.
XML could have a similar approach although I'm not sure if anyone has done it already.
Second talk (30 minute mark) of this video, https://www.youtube.com/watch?v=ld9rwCvGdhc
I've posted a few reasons before. I think I've refined the list slightly since last time:
* People's first exposure to programming often came from using C++ or Java. An old version with really crappy type errors. Schools are often conservative about updating their tech stacks.
* Types are most useful when reading or changing code. New learners are mostly writing new code.
* Writing `Person person = new Person()` seems highly redundant. In the kinds of small programs you are writing as a newbie, you are likely to write a lot of this.
The reasons so far make types seem like overhead: you are having to do more work and getting little in return for doing so. The next two get a bit deeper.
* In the small codebases you'll have as a newbie[0] at disproportionate amount of the codebase is interacting with the outside world. The outside world is untyped. In both typed or dynamic languages, you have to shuttle this untyped data into your language's type system. But when there is a type error in this process, I find it is generally easier to debug in a dynamic language. That makes sense to me: they need to have good workflows for dealing with runtime type errors.
* Classes tend not to teach technique[1]. Students are expected to invent it on their own as they learn programming. As professionals, we often don't teach technique to each other either. If you invent techniques that leverage the strengths of types, then the appeal of types will seem pretty obvious. If you don't you may go years without before you are exposed to these techniques. If you invent techniques where static types get in the way, then you may find static types to be a severe hindrance to getting things done.
[0] I think this also applies a lot of the time when starting a new project.
[1] By technique I mean the steps you do to produce working code. This doesn't just include generating new code, but understanding existing code and debugging code.
Think for example a library like Pandas. Building something like that with a not-very-flexible type system would result in much more cumbersome user experience. In many cases you would likely feel the types just getting on your way while working interactively.
Microsoft has done great things with C# on this frontier, but it has also taken many years and probably a lot of brainpower.
If my project is something beyond a small script that I plan on working on on or off for a while, I do find that annotations definitely help. Also, it fuels IDE completions between functions if you annotate your input.
- you can use list[] instead of typing.List[]. Same for dicts or sets.
- you will be able to use bool | str instead of typing.Union[bool, str]
- mypy has saner default, is better supported by IDE and is way faster
- a lot of edge cases are now covered, including protocols for duck typing, vartype, etc.
- fantastic libs such as pydantic, fastapi and typer make using them a ton of fun
However, mypy is woefully limited when compared to TypeScript. Granted, TypeScript is maintained by a trillion dollar company while mypy is a community project.
One particularly interesting (though in my experience, rare) class of bugs are typing errors _in unit tests_. For example, an API under test expects one thing and a unit test supplies something else. If the test passes, it's hard to spot the problem without static type checking.