Function types

We write Func(S): T for the type of functions that take a parameter of type ${\it {S}}$ and return a result of type ${\it {T}}$. If ${\it {{\it Func(S'):\ T'} {\rm \ <: \ }{\it Func(S):\ T}}}$, then we should be able to use an element of the first functional type in any context in which an element of the second type would type check.

  

Figure 2: A function ${\it {f:\ {\it Func(S):\ T}}}$, and ${\it {f':\ {\it Func(S'):\ T'}}}$ masquerading as ${\it {f}}$.

Suppose we have a function ${\it {f}}$ with type Func(S): T. In order to use an element, ${\it {f'}}$, of type ${\it Func(S'):\ T'}$ in place of ${\it {f}}$, the function ${\it {f'}}$ must be able to accept an argument of type ${\it {S}}$ and return a value of type ${\it {T}}$. See Figure 2. But ${\it {f'}}$ is defined to accept arguments of type ${\it {S'}}$. Now ${\it {f'}}$ can be applied to an argument, ${\it {s}}$, of type ${\it {S}}$ if ${\it {S {\rm \ <: \ }S'}}$. In that case, using subsumption, ${\it {s}}$ can be treated as an element of type ${\it {S'}}$, making ${\it {f'(s)}}$ typable. Similarly, if the output of ${\it {f'}}$ has type ${\it {T'}}$ then ${\it {T' {\rm \ <: \ }T}}$ will guarantee that the output can be treated as an element of type ${\it {T}}$. Summarizing,

$${\it Func(S'):\ T'} {\rm \ <: \ }{\it Func(S):\ T} \mbox{ if... ...S'}}} \mbox{ and } {\rm{\it {T'}}} {\rm \ <: \ }{\rm{\it {T}}}.$$

Again assuming that ${\it {TropicalFruit {\rm \ <: \ }Fruit}}$, we get that

$${\rm{\it {{\it Func(Integer):\ TropicalFruit} {\rm \ <: \ }{\it Func(Integer):\ Fruit}}}},$$

but

$${\rm{\it {{\it Func(Fruit):\ Integer} {\rm \ <: \ }{\it Func(TropicalFruit):\ Integer}}}}.$$

Procedure types, written ${\it {Proc(S)}}$, may be subtyped as though they were degenerate function types that always return a default type ${\it { Unit}}$, which has only a single value. Thus

$$Proc(S') {\rm \ <: \ }Proc(S) \mbox{ if } {\rm{\it {S}}} {\rm \ <: \ }{\rm{\it {S'}}}.$$

Notice that the ordering of parameter types in function and procedure subtyping is the reverse of what might initially have been expected, while the output types of functions are ordered in the expected way. We say that subtyping for parameter types is contravariant (i.e., goes the opposite direction of the relation being proved) while the subtyping for result types of functions is covariant (i.e., goes in the same direction). The contravariance for parameter types can be initially confusing, because it is permissible to replace an actual parameter by another whose type is a subtype of the original. However the key is that in the subtyping rule for function types it is the function, not the actual parameter, which is being replaced.