More explicitly document the type system

[JSAbrahams]

Many type system features are now kind of clear, but not wholly.
In the sense that I have a broad sense of what I want to achieve, but many design decisions are left vague.
Luckily, there's a lot of work on type systems done over the decades which we can leverage.
We should more completely document the type system to:

• Guide our testing efforts, to make sure that we implement what we say we implement.
• Guide our roadmap, what features we want and what we don't want to allow at all.

In a general sense, our guiding philosophy is that Mamba should be as flexible as possible.
We are not implementing a systems language, so we don't have to worry as much about stack vs. heap shenanigans.
But, if the check stage passes, then the application should be well-typed, in the sense that (not exhaustive perse but close I assume):

• We only call functions which exist.
• We only use types which exist.
• We only call methods if a variable's type declares said method.
• We only pass arguments to functions and methods which are (sub)types of the types declared in the signature.

Implicitly the above also ensures that:

• All variables' types are known at compile/transpile time.

Of course, we can't always guarantee the above if we call Python code.
For that we need an unsafe operator, see:

• Add operator for calling unsafe Python code #160

Questions such as:

• Is it static vs. dynamic (the former)
• Is it manifest vs. inferred (the latter)
• Do we use nominal or a structural type system (ideally the former but are there some situations where we accidentally allow the latter?)
• Do we use duck typing?
  We do in some situations check only that a type implements a method, but does that actually mean we perform duck typing?
  Do we do it to a limited extent, or not at all (but still static of course).

What about the following?

• Abstract
• Dependent
• Flow-sensitive
• Gradual
• Intersection
• Latent
• Refinement
• Substructural
• Unique
• Session