So it starts from the generic untyped lambda calculus and then shows that it is possible to reach erroneous states: so far so much like any dynamically typed language (so javascript, lua, python). Bear in mind javascript is also quite weakly typed, but that doesn't matter much for the point I am trying to elucidate.
You introduce types to try to describe the program state in a way that a static analyser is able to prove that the program will not reach erroneous states. You learn that types limit computing: the simply typed lambda calculus always halts. Note that a human reader is a type of static analyser.
You start introducing more advanced types to try to get back that unbounded possibility: to be a real programming language, you need the halting problem--a real server doesn't halt.
Anyways, after some chapters you learn that you may need a lot of rather advanced type theory to truly describe some of the complex things that some crazy people did in previously dynamically typed languages. That's why python type hints and typescript sometimes (but not usually) need some really crazy stuff: people were able to and did do all kinds of crazy things.
Arguably, there are easier ways to solve a problem than the way that requires advanced type theory to describe. The dynamic languages don't make it easier to write, verify and reason about such code other than the fact that many static languages prevent it outright.
You introduce types to try to describe the program state in a way that a static analyser is able to prove that the program will not reach erroneous states. You learn that types limit computing: the simply typed lambda calculus always halts. Note that a human reader is a type of static analyser.
You start introducing more advanced types to try to get back that unbounded possibility: to be a real programming language, you need the halting problem--a real server doesn't halt.
Anyways, after some chapters you learn that you may need a lot of rather advanced type theory to truly describe some of the complex things that some crazy people did in previously dynamically typed languages. That's why python type hints and typescript sometimes (but not usually) need some really crazy stuff: people were able to and did do all kinds of crazy things.
Arguably, there are easier ways to solve a problem than the way that requires advanced type theory to describe. The dynamic languages don't make it easier to write, verify and reason about such code other than the fact that many static languages prevent it outright.