# Why F-bounded polymorphism and F-bounded quantification are called, well, F-bounded

It's claimed in Wikipedia that:

F-bounded quantification or recursively bounded quantification, introduced in 1989, allows for more precise typing of functions that are applied on recursive types. A recursive type is one that includes a function that uses it as a type for some argument or its return value

Here's the article which Wikipedia refers to, and F-bounded quantification is introduced in that article in following fashion:

F-bounded quantification is a natural extension of bounded quantification that seems particularly useful in connection with recursive types.

My question is - why though it's F-bounded, what does "F" stands for in this particular context?

It appears that "F" does not stand for anything in particular: rather, it is the metavariable symbol that is used in the definition of F-bounded quantification. In the paper in which F-bounded quantification was introduced, F-Bounded Polymorphism for Object-Oriented Programming, the authors write:

To solve this problem and related difficulties with other forms of recursive types we introduce a generalization of bounded quantification which we call F-bounded quantification, for want of better terminology.

suggesting that they do not view the name as particularly descriptive. Later, when they define F-bounded quantification explicitly, they write:

We say that a universally quantified type is F-bounded if it has the form $$\forall t \subseteq F[t] . \sigma$$ where $$F[t]$$ is an expression, generally containing the type variable $$t$$.

As far as I can tell, the paper contains no other explanation and the most apparent explanation is that the "F" in the terminology is chosen to coincide with the symbol $$F$$ chosen, arbitrarily, for the definition.

• I see. I just thought that may be F has some well-recognised meaning in this domain, like you know, N or Z, so no additional explanation required. Apr 12, 2020 at 21:43