0
$\begingroup$

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?

|cite|improve this question
$\endgroup$
0
$\begingroup$

Consider these assertions:

  1. all the cats in my house are grey
  2. 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<: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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – ixampal Oct 21 '18 at 3:45
  • $\begingroup$ @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. $\endgroup$ – chi Oct 21 '18 at 7:57
  • $\begingroup$ Thanks for confirming. I was intuitively on board with the typing rule for Full F<: from the discussion on contravariance with arrow types. My confusion came from somehow looking at the "stronger constraint" in the explanation text as referring to something limiting the types X can take, not the whole programs. Missing the forest for the trees. All good now. $\endgroup$ – ixampal Oct 21 '18 at 8:13

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.