Go backward to Subtyping Go up to Top Go forward to Denotational Semantics

Minimal Types

• Coercion rule
  • pi |- 2: real
  • pi |- 2+4.5: realexp
• Unicity of typing is lost:
  • pi |- 2+3: intexp
  • pi |- 2+3: realexp
• Minimal type of every expression:
  • pi |- U: theta₁
  • theta₁ <= theta₂, for all pi |- U: theta₂
  • Attach each tree node with minimal type!
• Minimal type may not exist:
  • nonnegative <= int
  • nonpositive <= int
  • 0: nonnegative, 0: nonpositive