Go backward to Minimal Types Go up to Top Go forward to Extension of Subtyping

Denotational Semantics

• Meaning of subtyping relation
  • [[theta₁ <= theta₂]]: [[theta₁]] -> [[theta₂]]
  • Coercion map must exist.
  • [[theta <= theta]] is identity function.
  • [[theta₁ <= theta₃]] = [[theta₂ <= theta₃]] o [[theta₁ <= theta₂]]
  • [[pi |- E: theta₂]]e s = [[theta₁ <= theta₂]]([[pi |- E: theta₁]]e s)
• Semantics must be coherent
  • Meaning of well-typed program independent of derivation used to assert well-typing.
• Subtyping on objects:
  • {I₁:theta₁,...,I_m:theta_m,...,I_n:theta_n} <=
          {I₁:theta₁',...,I_m:theta_m'}
       if 0 <= m <= n and theta_j <= theta_j' for all 1 <= j <= m
  • [[{I₁:theta₁,...,I_m:theta_m,...,I_n:theta_n} <=
          {I₁:theta₁',...,I_m:theta_m'}]]
       {I₁=v₁,...,I_m=v_m,...,I_n=v_n}
    = {I₁=[[theta₁<=theta₁']]v₁,...,[[theta_m<=theta_m']]v_m}