docs: Clarify important points about parametric types

Closes JuliaLang#43811.

Removed some of the jargon and wikipedia links to make room for
a brief alternative `Point{T1,T2}` demonstration.
Shifted some paragraphs around to reflect their importance,
and changed the wording in some places.

Author: adigitoleo

doc/src/manual/types.md

@@ -539,26 +539,34 @@ See [this FAQ entry](@ref faq-nothing) for more information.
 
 An important and powerful feature of Julia's type system is that it is parametric: types can take
 parameters, so that type declarations actually introduce a whole family of new types -- one for
-each possible combination of parameter values. There are many languages that support some version
-of [generic programming](https://en.wikipedia.org/wiki/Generic_programming), wherein data structures
-and algorithms to manipulate them may be specified without specifying the exact types involved.
-For example, some form of generic programming exists in ML, Haskell, Ada, Eiffel, C++, Java, C#,
-F#, and Scala, just to name a few. Some of these languages support true parametric polymorphism
-(e.g. ML, Haskell, Scala), while others support ad-hoc, template-based styles of generic programming
-(e.g. C++, Java). With so many different varieties of generic programming and parametric types
-in various languages, we won't even attempt to compare Julia's parametric types to other languages,
-but will instead focus on explaining Julia's system in its own right. We will note, however, that
-because Julia is a dynamically typed language and doesn't need to make all type decisions at compile
-time, many traditional difficulties encountered in static parametric type systems can be relatively
-easily handled.
-
-All declared types (the `DataType` variety) can be parameterized, with the same syntax in each
-case. We will discuss them in the following order: first, parametric composite types, then parametric
-abstract types, and finally parametric primitive types.
+each possible combination of parameter values. This is often referred to as "generic programming".
+There are two kinds of explicitly declared parametric types.
+[Parametric composite types](#man-parametric-composite-types)
+declare a family of concrete, [composite types](#Composite-Types),
+whereas [parametric abstract types](#Parametric-Abstract-Types)
+declare a family of [abstract types](#man-abstract-types).
+Other kinds of built-in parametric types such as tuple types are discussed in this section as well.
+Parametric types can also be used in [type annotations](#Type-Annotations).
+
+!!! note
+    Parametric types do not represent a single node in the type graph.
+    Therefore, [`typeof`](@ref) can never return a parametric type name.
+    To dynamically verify a (parametric) subtype relation, use [`isa`](@ref) instead.
+
+!!! warning
+    Type parameters are invariant: even though `Float64 <: Real`,
+    the relation `Foo{Float64} <: Foo{Real}` does NOT hold for any parametric type `Foo`.
+    However, `Foo{Float64} <: Foo{<:Real}` is `true`.
+    This subtle but important point is the reason for the common use of
+    `Container{<:Element}` syntax in type annotations.
 
 ### [Parametric Composite Types](@id man-parametric-composite-types)
 
-Type parameters are introduced immediately after the type name, surrounded by curly braces:
+!!! note
+    For any parametric composite type,
+    both [`isabstracttype`](@ref) and [`isconcretetype`](@ref) will return false.
+
+Type parameters are introduced immediately after the type name, and surrounded by curly braces:
 
 ```jldoctest pointtype
 julia> struct Point{T}
@@ -567,13 +575,13 @@ julia> struct Point{T}
        end
 ```
 
-This declaration defines a new parametric type, `Point{T}`, holding two "coordinates" of type
-`T`. What, one may ask, is `T`? Well, that's precisely the point of parametric types: it can be
-any type at all (or a value of any bits type, actually, although here it's clearly used as a type).
-`Point{Float64}` is a concrete type equivalent to the type defined by replacing `T` in the definition
-of `Point` with [`Float64`](@ref). Thus, this single declaration actually declares an unlimited
-number of types: `Point{Float64}`, `Point{AbstractString}`, `Point{Int64}`, etc. Each of these
-is now a usable concrete type:
+This declaration defines a new parametric type, `Point{T}`,
+holding two "coordinates" of the same type `T`.
+The parameter `T` is a placeholder, which will be replaced by a particular concrete type
+when an instance of this type is created.
+Thus, this single declaration actually declares an unlimited number of types:
+`Point{Float64}`, `Point{AbstractString}`, `Point{Int64}`, etc.
+Each of these is now a usable concrete type:
 
 ```jldoctest pointtype
 julia> Point{Float64}
@@ -583,11 +591,8 @@ julia> Point{AbstractString}
 Point{AbstractString}
 ```
 
-The type `Point{Float64}` is a point whose coordinates are 64-bit floating-point values, while
-the type `Point{AbstractString}` is a "point" whose "coordinates" are string objects (see [Strings](@ref)).
-
-`Point` itself is also a valid type object, containing all instances `Point{Float64}`, `Point{AbstractString}`,
-etc. as subtypes:
+`Point` itself is also a valid type object,
+containing all instances `Point{Float64}`, `Point{AbstractString}`, etc. as subtypes:
 
 ```jldoctest pointtype
 julia> Point{Float64} <: Point
@@ -597,17 +602,7 @@ julia> Point{AbstractString} <: Point
 true
 ```
 
-Other types, of course, are not subtypes of it:
-
-```jldoctest pointtype
-julia> Float64 <: Point
-false
-
-julia> AbstractString <: Point
-false
-```
-
-Concrete `Point` types with different values of `T` are never subtypes of each other:
+Concrete `Point` variants with different values of `T` are never subtypes of each other:
 
 ```jldoctest pointtype
 julia> Point{Float64} <: Point{Int64}
@@ -617,13 +612,9 @@ julia> Point{Float64} <: Point{Real}
 false
 ```
 
-!!! warning
-    This last point is *very* important: even though `Float64 <: Real` we **DO NOT** have `Point{Float64} <: Point{Real}`.
-
-In other words, in the parlance of type theory, Julia's type parameters are *invariant*, rather
-than being [covariant (or even contravariant)](https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29). This is for practical reasons: while any instance
-of `Point{Float64}` may conceptually be like an instance of `Point{Real}` as well, the two types
-have different representations in memory:
+In other words, in the parlance of type theory, Julia's type parameters are *invariant*.
+This is for practical reasons: while any instance of `Point{Float64}` may conceptually be
+like an instance of `Point{Real}` as well, the two types have different representations in memory:
 
   * An instance of `Point{Float64}` can be represented compactly and efficiently as an immediate pair
     of 64-bit values;
@@ -632,9 +623,9 @@ have different representations in memory:
     practice an instance of `Point{Real}` must be represented as a pair of pointers to
     individually allocated `Real` objects.
 
-The efficiency gained by being able to store `Point{Float64}` objects with immediate values is
-magnified enormously in the case of arrays: an `Array{Float64}` can be stored as a contiguous
-memory block of 64-bit floating-point values, whereas an `Array{Real}` must be an array of pointers
+The efficiency gained by imposing this restriction is magnified enormously in the case of arrays:
+an `Array{Float64}` can be stored as a contiguous memory block of 64-bit floating-point values,
+whereas an `Array{Real}` must be an array of pointers
 to individually allocated [`Real`](@ref) objects -- which may well be
 [boxed](https://en.wikipedia.org/wiki/Object_type_%28object-oriented_programming%29#Boxing)
 64-bit floating-point values, but also might be arbitrarily large, complex objects, which are
@@ -663,8 +654,7 @@ end
 
 More examples will be discussed later in [Methods](@ref).
 
-How does one construct a `Point` object? It is possible to define custom constructors for composite
-types, which will be discussed in detail in [Constructors](@ref man-constructors), but in the absence of any special
+How does one construct a `Point` object? In the absence of any special
 constructor declarations, there are two default ways of creating new composite objects, one in
 which the type parameters are explicitly given and the other in which they are implied by the
 arguments to the object constructor.
@@ -724,8 +714,23 @@ Closest candidates are:
   Point(::T, !Matched::T) where T at none:2
 ```
 
-Constructor methods to appropriately handle such mixed cases can be defined, but that will not
-be discussed until later on in [Constructors](@ref man-constructors).
+For that to work, we could change our definition of the `Point` type:
+
+```jldoctest
+julia> struct Point{T1,T2}
+           x::T1
+           y::T2
+       end
+
+julia> p = Point(1, 2.5)
+Point{Int64, Float64}(1, 2.5)
+
+julia> p2 = Point(1, 2)
+Point{Int64, Int64}(1, 2)
+```
+
+Constructor methods to appropriately handle more complex cases can also be defined, 
+see the [Constructors](@ref man-constructors) section.
 
 ### Parametric Abstract Types