A useful intuition is the one you described: the code of a parametric-polymorphic function
f can not access type
T and choose to behave in different ways according to what
f the values of type
T are opaque:
f can interact with those values only in very restricted ways. For instance,
f can "move them around":
f : <T,U> (T,U) -> (U,T)
f (t,u) = (u,t)
f swaps the pair "moving" their components, but does not really interact with those.
f can also interact with the values exploiting its arguments
f : <T> (T, T->Bool) -> Int
f (t,g) = if g(t) then 4 else 6
f interacts with
t, but only through function
g which is passed as an argument.
A precise formalization of the behavior of functions whose behavior (roughly) does not "depend on
T" was given by Reynolds when he studied parametricity and proved the abstraction theorem. This is a bit complex in the general case, but one can grasp some ideas from the following example.
List(T) denote a type for finite sequences of values
[t1,...,tn] of type
T. In particular, given any function
g : T -> U, we can "lift" this to lists and obtain
map g : List(T) -> List(U) by letting
map g([t1,...,tn]) = [g(t1),...,g(tn)]
For instance, if
g : Int -> Int is defined as
map g : List(Int) -> List(Int) will increment each value of its input:
map g([x1,..,xn]) = [x1+1,...,xn+1].
Finally, consider a parametric-polymorphic function
f : <A> List(A) -> List(A)
and assume that, when
A = Int we have
f<Int> ([1,2,3]) = [2,1,1]
f is parametric-polymorphic. So,
f did not really "know" that
1 was number one -- it did not even "know" it was an integer. Consequently, if we replace
1 with any value
2 with any value
3 with any value
z, all of type
f has to satisfy
f<T> ([x,y,z]) = [y,x,x]
This can be further generalized as follows:
for any g : T -> U
f<U> (map g(list)) = map g(f<T> (list))
which reads as: if we affect the elements of the input list elements using
g before calling
f, we get the same result as calling
f first, and then affect the output list elements using
g. Intuitively, this has to be the case, since
f can not "read" the elements, but can only "move them around", "duplicate them", or "discard them".
(In category theory, that's called a "naturality property")
Note that, in virtue of the above property, if we need to test a list-reversal parametric-polymorphic function
reverse : <T> List(T) -> List(T)
we can simply choose
T = Int, and test for lists of integers
[1,2,...,n], only. That's because if the function reverses those lists of integers, it will reverse any other list (even those having a different element type).
You may want to convince yourself that the above property can be generalized to all "cointainer" types (lists, pairs, trees, ...). Parametricity goes beyond that, but that's a good example in my mind.
The "theorems for free!" paper by Wadler is a classic introduction to parametricity and contains further examples.