Type Systems for Modules (Winter 2010)

Course Information

Lecture type:	Seminar, 7 CPs (?)
Time:	Mon, 4-6pm
Room:	MPI-SWS (Wartburg) in 304
Instructor:	Derek Dreyer

Description

Module systems are central to the construction of large-scale programs, and there is a rich and highly-developed theory devoted to the study of type systems for modules. In this seminar course, we will focus attention on the origins, design, semantics and implementation of the ML module system, one of the most influential and highly evolved module systems available. We will investigate the numerous issues that arise in formalizing ML modules, as well as the different styles of formalization (e.g. ad-hoc, direct-style, elaboration), and we will also study a variety of challenging extensions to the ML module system, including higher-order functors and recursive modules.

There will be one 2-hour lecture per week. Students will be expected to read 1-2 papers per week and to participate in a lively class discussion. There will also be a relatively lightweight class project (e.g. writing a short survey paper or preparing a lecture on advanced material, implementing an advanced module system design). The course is taught in English, and is intended for students who have already taken a course in semantics and/or type systems for programming languages.

Schedule

Date	Description / Reading	Leader, Questions	Scribe, Notes
Mon, Oct 18	Introduction to the seminar.
Mon, Oct 25	Using types to describe modules. Mitchell and Plotkin. Abstract Types Have Existential Type, TOPLAS 1988, originally in POPL 1985. MacQueen. Using Dependent Types to Express Modular Structure, POPL 1986. Harper and Mitchell. On the Type Structure of Standard ML, TOPLAS 1993, originally in POPL 1988.	Scott txt link	Scott pdf link
Tue, Nov 2 12:15 to 2:00	Manifest types and translucent signatures. Leroy. Manifest Types, Modules, and Separate Compilation, POPL 1994. Harper and Lillibridge. A Type-Theoretic Approach to Higher-Order Modules with Sharing, POPL 1994.	Beta txt link	Scott pdf link
Mon, Nov 8 12:15 to 2:00	Module type systems based on System F. Russo. Non-Dependent Types for Standard ML Modules, PPDP 1999. Rossberg, Russo, and Dreyer. F-ing Modules, TLDI 2010. Auxiliary reading: Harper and Stone. A Type-Theoretic Interpretation of Standard ML, Milner Festschrift, 2000. Harper and Stone. An Interpretation of Standard ML in Type Theory, Tech Report, 1997.	Jonas txt link	Sigurd pdf link
Mon, Nov 15	More on functors. Only read Chapter 1 of Dreyer's thesis. Leroy. Applicative Functors and Fully Transparent Higher-Order Modules, POPL 1995. Dreyer. Understanding and Evolving the ML Module System, PhD thesis, 2005.	Sigurd txt link	Beta (none yet)
Mon, Nov 22	Unified framework for both generative and applicative functors. Keep working on last week's questions, too. Dreyer, Crary, Harper. A Type System for Higher-Order Modules, POPL 2003.	Derek (none yet)	Jonas (none yet)
Wed, Dec 1 6:15 to 8:00	Classifications of modules by purity. Continuation of Dreyer's thesis (Chapter 2). Dreyer. Understanding and Evolving the ML Module System (Chapter 2), PhD thesis, 2005.	Derek txt link	Jonas (none yet)
Mon, Dec 6	Recursive modules are harder than you think. Bring the auxiliary papers to class with you, whether you read them or not. Dreyer. Understanding and Evolving the ML Module System (Chapter 5), PhD thesis, 2005. Auxiliary reading: Flatt, Felleisen. Units: Cool Modules for HOT Languages, PLDI 1998. Crary, Harper, Puri. What is a Recursive Module?, PLDI 1999. Russo. Recursive Structures for Standard ML, ICFP 2001.	Derek (none yet)	Georg pdf link
Mon, Dec 13	You can skip most of the metatheory details for now (Section 4), and focus on the other sections. Dreyer. Recursive Type Generativity, JFP 2007, previously in ICFP 2005.	Derek (none yet)	Gil (none yet)
Mon, Jan 3	Recap and question time.
Mon, Jan 10	More on recursive modules. Dreyer. A Type System for Recursive Modules, ICFP 2007.	(none yet)	(none yet)
Mon, Jan 17 12:15 to 2:00	Mixin modules. Only read Sections 1-3 of the MixML paper. Print out and take a quick look at the Owens and Flatt paper, too. Dreyer and Rossberg. Mixin' Up the ML Module System, ICFP 2008. Auxiliary reading: Owens and Flatt. From Structures and Functors to Modules and Units, ICFP 2006.	(none yet)	(none yet)
Mon, Jan 24 cancelled	Cancelled due to POPL conference.
Wed, Feb 2 6:15 to 8:00	MixML. Dreyer and Rossberg. Mixin' Up the ML Module System, ICFP 2008.	(none yet)	(none yet)
Mon, Feb 7	Finish discussing MixML. Dreyer and Rossberg. Mixin' Up the ML Module System, ICFP 2008.	(none yet)	(none yet)

Likely Topics for the Seminar

• Origins of the ML module system
  • Existential types (Mitchell-Plotkin)
  • Dependent types (MacQueen, Harper-Mitchell)
• Design of the ML module system
  • Overview (Harper-Pierce, Dreyer)
  • Using ML modules in anger (Ramsey)
• Formalization of ML-style modules
  • Definition of Standard ML (Milner-Tofte-Harper-MacQueen)
  • Direct approach (Leroy, Harper-Lillibridge)
  • Elaboration approach (Harper-Stone)
  • Singleton kinds (Stone-Harper)
  • "F-ing modules" (Russo, Rossberg-Russo-Dreyer)
• Higher-order functors: applicative vs. generative
  • Direct approach (Leroy, Shao, Dreyer-Crary-Harper)
  • "F-ing modules" (Rossberg-Russo-Dreyer)
• Recursive modules
  • Early proposals (Crary-Harper-Puri, Russo)
  • Double vision problem (Dreyer)
  • Later proposals (Owens-Flatt, Nakata-Garrigue)
  • MixML (Dreyer-Rossberg)
• Other topics
  • Semantics of type generativity (Ahmed-Dreyer-Rossberg)
  • Dynamic type generativity (Rossberg, Neis-Dreyer-Rossberg)
  • Modular type classes (Dreyer-Harper-Chakravarty)

Last modified: July 03 2012 17:36:03