Today’s lecture gave examples of parameterized types in different programming languages: families of data types with a common structure, built by applying type constructors to one or more type parameters; as in Java or C# generics, or the algebraic datatypes of Haskell and OCaml. To work with parameterized types we use polymorphic functions — code that can work with more than one type, either in a uniform way (parametric polymorphism) or with type-specific variations (ad-hoc polymorphim).
The Hindley-Milner type system, illustrated in this lecture as applied to the simply-typed lambda-calculus, expands types into type schemes that summarize multiple possible types of a polymorphic function. Hindley-Milner is distinctive in guaranteeing that any code has a principal type scheme that captures every possible type, and the efficient Algorithm W for type inference which can find (“infer”) that most general type scheme.

Link: Slides for Lecture 3

Homework

1. Read This

Philip Wadler. Propositions as Types. Communications of the ACM, 58(12):75–84, December 2015.

Author page · PDF · Publisher page · HTML · PDF

There’s also a video of Prof. Wadler’s presentation at Strange Loop 2015.

Link: Propositions as Types

2. Code This

Java has subtyping: a value of one type may be used at any more general type. For example, String ≤ Object, and every Java String is an Object. This isn’t always straightforward — consider the following code.

String[] a = { "Hello", "world" }; 
Object[] b = a;                    
b[0] = Boolean.FALSE;              
String s = a[0];                   
System.out.println(s.toUpperCase());

1. Build a Java program around this.
2. Compile it.
3. Run it.
4. What happens? Can you explain why?
5. How might you change the Java language to prevent this?

References

	GJ: A Generic Java Language Extension Wadler’s page recording the development of Java generics, and their eventual inclusion into the language. Links: GJ web page; Generics today: Java tutorial
	Generics for .NET Andrew Kennedy’s page recording the development of .NET generics, and some of the work involved going from a theoretically clean and useful concept all the way to practical deployment in the .NET tools and runtime. Links: Kennedy on .NET generics; Don Syme’s whiteboard; Microsoft current generics documentation