## Type Annotations

Though we established that types and classes are basically the same
thing in Python, annotations are normally called «type annotations»
and not class annotations, even though they can in fact be
anything-annotations, as far as «Python» is concerned. This is valid
Python:

    def f() -> 3: pass                          # python

The code simply annotates the function's ‘return type’ to be 3 (not
the return «value» mind you; it's an annotation, not the result).
The interpreter only really cares that this is a valid expression
that it can (and will) evaluate at runtime (at the time the function
is defined)… try this:

    def f() -> print( 'hello' ): pass           # python

In any case, it is the job of an «external type checker» to make
sense of the annotations (and of course, both of the above will be
rejected by any sensible type checker). A typical example is ‹mypy›
(and to some extent, it is the «standard» type checker, but there
are others, e.g. ‹pyright›).

Now in the context of type systems, ‹mypy› is really 2 distinct
systems with somewhat distinct properties. First, let's consider
«strict» ‹mypy›, which is a more or less standard «static» type
system with both «subtyping» and «parametric polymorphism»; it is
also somewhat weak in the sense that:

 1. it has ‹cast› so that the programmer can (accidentally) lie
    about types,
 2. it can get things wrong on its own, because it relies on data
    flow analysis¹ to restrict «union types». If you call ‹g› in the
    following program, it dies with a ‹TypeError›, but ‹mypy
    --strict› will accept it as correct:
    
        x: None | int = 1                     # python

        def f() -> None:
            global x
            x = None
       
        def g() -> None:
            if x is not None:
                f()
                print( x + 1 )
    
    Certainly, this is not the outcome we have hoped for. Without
    the backing of Python's strong dynamic type system, we could
    have ended up in real hot water.

Now the other ‹mypy› mode, without the ‹--strict› switch, is «much
weaker» than the above. This is because any unannotated function or
variable is quietly accepted as correct, including any expressions
that make use of it. In non-strict mode, ‹mypy› will accept the
following:

    def h( x ):                               # python
        return x + 3

    h( 'foo' )

Which is not to say that ‹mypy›, even in the non-strict mode, is
useless: but it is important to understand the limitations. A
compromise solution is using ‹--strict› but allowing oneself to use
‹Any› as an annotation, which is a way of saying ‘I do not want to
annotate this function, but I am aware the type is not going to be
checked’. The latter two modes (non-strict and strict with ‹Any›)
are examples of «gradual typing».

¹ For the more theoretically inclined: data flow analysis is clearly
  undecidable in general. Of course it's always possible to try some
  heuristics and if the result is ‘don't know’ simply reject the
  program as ill-typed. Unfortunately, that makes the system awfully
  restrictive, inconvenient and basically useless to a working
  programmer.
