It encodes it into the type system at the function signature level. Optional[Int] is an Int with a None, so if you pass this type into f(x: Int) you get a type

It encodes it into the type system at the function signature level. Optional[Int] is an Int with a None, so if you pass this type into f(x: Int) you get a type error because f(x: Int) is a function that deals with Ints, not Optional[Int]. So you get a degree of safety here. As I mentioned this safety does not usually extend to the function definition. I stated that it can though (and it is in haskell and rust), and this is usually done through a feature called pattern matching. Pattern matching is available in python 3.10 but I'm not sure whether exhaustive type checking on pattern matching by external type checkers is available yet.