Go backward to Denotational Semantics Go up to Top Go forward to Subtyping of Function Types

Extension of Subtyping

• Other parts of programming language:
  • Subtyping on modules.
  • pi₁dec <= pi₂dec if pi₁ <= pi₂
  • fun A=2, proc A=skip
  • {A:intexp}dec <= {}dec
  • {A:comm}dec <= {}dec
  • {A:intexp}dec or {A:comm}dec?
  • Two different incorrect typings!
• Function types:
  • theta₁₁->theta₁₂ <= theta₂₁->theta₂₂
    if theta₂₁ <= theta₁₁ and theta₁₂ <= theta₂₂
  • Contravariance of argument and result types!
• Example:
  • TRUNC: realexp -> intexp
  • Result can be extended to realexp
  • Argument can be extended to realexp
  • TRUNC: intexp -> realexp!