Go backward to Overloading and Coercion Go up to Top Go forward to The Untyped lambda-Calculus

Preview of Fun

• lambda-calculus based language
  • Basis is first-order typed lambda-calculus.
  • Enriched by second-order features for modeling polymorphism and object-oriented languages.
• First-order types
  • Bool, Int, Real, String.
• Various forms of type quantifiers
  • Type ::= ...| Quantified Type
  • Quantified Type ::=
    forall A. Type |
    exists A. Type |
    forall A subsetType. Type | exists A subsetType. Type
• Modeling of advanced type systems:
  • Universal quantification: parameterized types.
  • Existential quantifiers: abstract data types.
  • Bounded quantification: type inheritance.