Function subtyping variance (source code)

= Function subtyping variance
{title2=$A\to B\;<:\;A'\to B'$}

If $A'<:A$ and $B<:B'$, a <function> of type $A\to B$ safely supplies a contract of type $A'\to B'$. Every input permitted by the new contract is already accepted, and every possible returned value meets the weakened result promise. The input constraint reverses <subtyping>, while the output constraint preserves <subtyping>. Reversing either direction can respectively supply an unsupported input or promise a result more specific than the implementation returns. A language's generic type <type constructor> may nevertheless be invariant unless its declaration exposes the appropriate <type variance>.