What Python and other dynamically typed languages call "types" aren't types at all in the theoretical sense. In type theory, types are properties ascribed to programs that describe their behavior and are part of a language's static semantics (AKA checked at compile time). Dynamically typed languages are really untyped (or from a certain perspective, "unityped," meaning that every expression has the same type: https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...).
Note many dynamically typed languages have static types. Objective-C, Java, TypeScript, Dart, etc. The dynamic types bring new capabilities above and beyond what is possible with static types.
(That is, the dynamic-or-static choice is a product type, not a sum type!)
> The dynamic types bring new capabilities above and beyond what is possible with static types.
Not really. "Dynamic type" just means an object that carries around a description of its structure (or more commonly, a pointer to a description). You can do the same thing in many languages with static types. (Including Haskell. GHC has special support for this pattern.)
GHC can derive a Typeable type class instance for any data type which allows values of that type to be stored in a Dynamic wrapper. For soundness reasons the Typeable type class is special in that it can only be derived; you can't implement it manually. The runtime types of Dynamic values can be queried and compared and you can attempt to extract a specific known (concrete) type, which will succeed only if the runtime type matches. There are some limitations; for example, you need to know the exact type of the value you're extracting, not just a type class constraint, so you can't e.g. add two Dynamic values directly even if they hold the same type of value at runtime with a valid Num instance.
Alternatively, you can just define a recursive sum type expressing all the possible runtime types of the dynamic expression. In Aeson for example there is a type which can encode any value which might be found in a JSON file, which is basically everything you can express in Javascript apart from function closures. This doesn't require any special support from GHC and works well in most statically-typed languages.
Haskell's unit type is what other languages call "void", the type with exactly one value (not counting 'undefined', Haskell's dirty little not-secret). That's different from Unitype/Any, the type that contains all values.
Bob Harper uses "unitype" which is a pretty strong argument for the name's validity
> not counting 'undefined', Haskell's dirty little not-secret
There is no "undefined" value in pure Haskell. There are expressions that have no value, due to a runtime exception (error, undefined, division by zero, memory allocation failure) or non-termination (unbounded recursion). Either way, evaluating the expression does not produce a value for the remainder of the program to operate on—you can't write a (pure) program like `if isUndefined expr then x else y` since—assuming isUndefined is a pure function and doesn't ignore its argument—the whole program is undefined if expr is undefined.
