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&lt;: (p. 395):


  A type T = ∀X&lt;: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&lt;: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?
Consider these assertions:


all the cats in my house are grey
all the cats in my town are grey


The second assertion implies the first, since any cat in my house is also in my town, so by the assertion it must be grey. In other words, "cats in my town" is a superset of "cats in my house", so the second assertion is stronger (it applies to more cats).

In the same way, the type S = ∀X&lt;:S1.T2 is stronger than T = ∀X&lt;: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.