# Bounded Quantification: Full F<: intuition

I'm currently looking into Chapter 26 of Types and Programming Languages and am a bit confused by the "intuition" for Full F<: (p. 395):

A type T = ∀X<:T1.T2 describes a collection of functions from types to values, each mapping subtypes of T1 to instances of T2. If T1 is a subtype of S1, then the domain of T is smaller than that of S = ∀X<:S1.S2, so S is a stronger constraint and describes a smaller collection of polymorphic values.

Why is S a stronger constraint due to the fact that T's domain is smaller than S's?

In the same way, the type S = ∀X<:S1.T2 is stronger than T = ∀X<:T1.T2 since S1 is a supertype of T1. A program of type S must work in all cases (types X) where a program of type T would work, and possibly even more cases.
• Thanks for your response, @chi. So, it's stronger because it means programs can make fewer assumptions about X? This might explain the bit about describing "a smaller collection of polymorphic values". Let's say S1 is Top, then we have values λX<:Top.t for some term t. In regard to X, t can only use the knowledge that X is a subtype of Top, so there are certain subterms that cannot appear in t, e.g. applying a value of type X to another. If λX<:(Top→Top).u, u could contain subterms of that form. Is that the correct explanation or line of thought? – ixampal Oct 21 '18 at 3:45
• @ixampal Yes, that looks correct. For instance, a program of type ∀X<:Top. X->X must be the identity, since there are no operations it can perform on the X-typed argument. Instead, ∀X<:U. X->X can use its argument according to the operations of U, so it might be the identity, but could also be something else. If U is a type that represents pairs of the same type, then a program could swap the pair components. – chi Oct 21 '18 at 7:57