Instructor: Kung Chen 陳恭

This unit introduce the development of type systems for modern programming languages with emphasis on functional and object-oriented languages. It aims to help students get familiar with the basic forms of polymorphism in modern programming languages. The topics to cover include the following:

• Intro. to type tystems
• Polymorphic type sytems for functional languages
  • The Hindley-Milner type system
  • Haskell’s type classes
  • The polymorphic lambda calculus
• Subtyping polymorphism for object-oriented languages
  • Subtyping basics
  • Bounded quantification
  • F-bounded quantification

• Slides
• Exercise 1. Solution distributed on paper.
• Exercise 2. Solution distributed on paper.

• Louis Damas and Robin Milner, Principal Type-Schemes for Functional Programs, In Proc. 9th Annual ACM Symposium on Principles of Programming Languages, pages 207-212. ACM, 1982.

• Wadler, P. and Blott, S., “How to make adhoc polymorphism less ad-hoc,” Proc. 16th ACM Symposium on Principles of Programming Languages, pp. 60–76, 1989.

• Mark P. Jones. A system of constructor classes: Overloading and implicit higher-order polymorphism. In Arvind, editor, Proc. Functional Programming Languages and Computer Architecture 1993, pages 52-61, Copenhagen, Denmark, June 1993. ACM Press, New York.

• Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. F-bounded quantification for object-oriented programming. In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 273–280, September 1989.