CIS 700-003: Parametric and Ad hoc Polymorphism
University of Pennsylvania

Spring 2006

Location: Towne 305
Time: Tuesday and Thursday 10:30 - 11:50 AM
Instructor: Stephanie Weirich
Prerequisites: CIS 500 (Software foundations) or permission of the instructor

[schedule] [topics]

An important principle of software construction is to factor out common functionality. Many programming languages use type abstraction, also called type polymorphism, to support this process.  With polymorphism, functions and procedures can operate over many different forms of data so that the same code can be used in many situations. Examples include:
  • data structures, such as lists and trees, that store and provide access to many different types of elements
  • run-time services, such as serialization, structural equality, and garbage collection, that iterate over any type of data
  • operations that apply to all types of data supporting a common interface
However, few programming languages support the rich forms of polymorphism needed for all of the above situations. Traditionally, polymorphism has been divided into three distinct flavors (parametric, ad hoc and subtype) and languages typically support only one or two of these varieties. It is becoming clear that all three of these forms of polymorphism are essential. Therefore, much current research seeks to integrate these forms of polymorphism together, and into next-generation programming languages.

In this course, we will investigate parametric and ad hoc polymorphism in detail. We will ask questions such as: What operations can they express? How can languages supporting them be mathematically modeled? What happens when they are combined together and with other language features? How does polymorphism relate to other mechanisms for software abstraction? Our sources for study will be recent research results in the field of programming languages as well as classic papers, tutorials and textbooks.

Recommended textbooks:
Benjamin C. Pierce, Types and Programming Languages.
Benjamin C. Pierce, ed. Advanced Topics in Types and Programming Languages

Schedule

Date
Topic
Notes
1/10
Overview

1/12*
System F
Brian Aydemir
TAPL 23 / 24
1/17
F-omega
TAPL 30 / Type-Safe Cast
1/19
Parametricity
Theorems for Free
1/24*
Parametricity proof
Geoff Washburn
1/26*
HM Type inference
Dimitrios Vytiniotis
Practical type inference for arbitrary-rank polymorphism
1/31
Arbitrary-rank polymorphism
Practical type inference for arbitrary-rank polymorphism
2/2
Existential types
Type classes with existential types
exists0.hs
exists1.hs
exists2.hs
2/7
Value restriction in ML
First-class existentials (a crazy idea)
Simple, partial type inference for System F
based on type containment

2/9
Impredicative polymorphism
Boxy types: inference for higher rank types and impredicativity
2/14
and
2/16
Constraint-based type inference
The essence of ML type inference (ATTAPL Ch. 10)
2/21
Type classes (intro)
Jeff Vaughan
Type classes in Haskell
Type classes: Exploring the design space
2/23
Programming with type classes Justin Smith
Strongly typed heterogeneous collections
2/28
and
3/2
Multiparameter type classes Understanding functional dependencies via Constraint Handling Rules
3/7
none
Spring break
3/9
none
Spring break
3/14
More multiparameter type classes Monadic interpreter
3/16
More multiparameter type classes Karl Mazurak
Associated type synonyms
3/21
and
3/23
Programming with GADTs Aaron Bohannon
Putting Curry-Howard to work
3/28
Unifying type classes and GADTs (via CHRs) Brian Aydemir
A framework for Extended Algebraic Datatypes
3/30
Type-directed programming
Intensional Type Analysis in Type-Erasure Semantics
lambda-r.om
4/4
HO type-directed programming
Polytypic values possess polykinded types
gh-examples.ghs
4/6
Generic Haskell
Generic Haskell, Specifically
gh-spec.ghs
lambda-r-con.om
4/11
Run-time HO Type analyis
Type-Safe Run-time Polytypic Programming
gadt-impl.hs
gadt-impl2.hs
4/13
SYB (I)
Scrap your boilerplate with class: extensible generic functions
ShrinkIdeal.hs
ShrinkStandAlone.hs
Shrink.hs
4/18
SYB (II)
Scrap your boilerplate reloaded
4/20
Course overview

*indicates dates when Prof. Weirich will be away.

Topics and Resources

This class will draw on some of the same material as CIS 670 / Fall 2002.

For concreteness, we will look at many of these topics in the context of the Haskell programming language. However, we will not spend a lot of time covering Haskell in class--students will be expected to read about and play with Haskell on their own.
  1. Haskell
  2. Explicit parametric polymorphism
    • Universal types 
    • Existential types 
    • Higher-order polymorphism
    • Parametricity
  3. Implicit parametric polymorphism
    • Hindley-Milner type inference
    • Existential types in Haskell
    • Arbitrary-rank polymorphism
    • Boxy type inference
    • HM(X)
  4. Haskell type classes + extensions
    • Constructor classes
    • Multiparameter classes and functional dependencies
    • Associated types
    • Programming with type classes
  5. Type-directed programming
    • GADTs
    • Run-time type analysis in Haskell
    • Scrap your boilerplate
    • Generic Haskell