Go backward to Dynamically Scoped Objects Go up to Top Go forward to Minimal Types

Subtyping

• Typing system that formalizes subtyping:
  • Type attributes theta₁ <= theta₂
  • theta₁ is subtype of theta₂
  • Phrase of type theta₁ can be used in any context that demands phrase of type theta₂.
  • <= is reflexive and transitive.
• Example: mixed mode arithmetic.
  • int <= real
  • tau₁ <= tau₂ => tau₁exp <= tau₂exp.
• Typing rules:

  • pi |- E: theta1

    pi |- E: theta2

    if theta₁ <=theta₂

  • pi |- E1: tauexp	pi |- E2: tauexp
    pi |- E1+E2: tauexp

  • pi |- E: tau

    pi |- E: tauexp

    tau in{int, real}

  • pi |- N: int

    pi |- N1.N2: real