Suppose I take a relational view of types and polymorphism (which is quite natural given Reynold's work on relational parametricity.) Then, rather than thinking of a polymorphic type, that is a type (usually) represented by a free variable ranging over types, as free, I believe that it is better to think of it as unconstrained. Of course, unconstrained is the double-negation of free!
But since this is CS, it is useful to think constructively, so that these do not necessarily correspond. This is doubly natural since we know that the usual formalisms for parametric polymorphism do not have models in Set.
Which allows us to switch to viewing types in a relational setting. If we think of the usual lattice of types as our 'points', then the usual way of looking at (principal) types is that we want the least-upper-bound (in the 'information order' induced by the Scott topology) of all the typings, with this LUB being a valid type as well (where we use continuity to achieve that). So the space of points is not uniform like Euclidean space, but rather layered.
But what if stop thinking of Euclidean space in terms of points and switch to looking at it through the eyes of the Zariski topology? Well now Euclidean space starts to look rather layered too! And how does one explain the layers? Well, via ideals. More precisely, via systems of polynomials. But, in this setting, what is a principal ideal? It is one which is generated by a single element -- just like a principal type!
If we are to take any lesson at all from algebraic geometry, it is that to really study varieties, one needs to switch away from looking at sets-of-points, and study ideals very carefully. By analogy, the lesson should be to stop looking at types themselves, and to focus instead on the constraints which engender them. Then types are just the solutions to these constraint equations. In fact, one can even learn more from algebraic geometry and see that a lot of systems of constraints can be interpreted in multiple contexts (yes, I refrained from saying that they are polymorphic); and in each context, these systems can possess different solution 'sets'.
Rather than using Ring-theoretic methods, it might be better to focus on Lattice-theoretic methods, since Relation Algebras (seen as operators acting on the lattice of types) have a more natural ideal structure arising from its (residuated) lattice structure rather than its interpretation as an idempotent ring. But the ideas are still fundamentally the same.
In other words, a polymorphic type should be seen as the 'solution' to the empty relation. Principal types occur when a relation is fully triangularizable. This correspondance between the solutions-of-relations and types really needs a full blog post (if not a paper) to explain and spell out properly. But I wanted to jot down the line of reasoning, because it escaped me again.
