Beyond the simply-typed lambda-calculus, and even Hindley-Milner polymorphism, there’s a world of type systems for more expressivity, more precision, and more polymorphism. Today’s lecture looked at some of this: issues around subtype polymorphism in object-oriented code, motivations for higher-rank polymorphism, and beyond that to System F. For System F in particular there’s a range of further possibilities: this lecture covered encoding datatypes, but there are also subtyping, bounded and F-bounded quantification, F2, Fω, existential types, and more…
Link: Slides for Lecture 4
Homework
1. Read This
The written coursework assignment for APL this semester is to investigate one of five programming-language topics and write a 10-page report on it. During next Tuesday’s lecture I shall give a brief overview of each topic, and explain more about what’s involved in the assignment. Before then, download and read the assignment handout.
Link: APL coursework
Please note two additional points.
- Alternate topics may be allowed. If you wish to propose one then please send me a title and a short paragraph on what you would like to investigate for your report.
- I hope to arrange feedback for the preliminary submissions through guided peer assessment in small groups during one lecture slot.
Both of these are new for the course this year, and may be subject to change.
2. Do This
Work through the items on the slide “Exercises for the Reader” in today’s lecture, exploring encoding of datatypes in System F.
References
 |
Interfaces and specifications for the Smalltalk-80 collection classes William R. Cook In OOPSLA ’92: Proceedings of the Seventh Annual Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM Press, 1992. DOI: 10.1145/141936.141938 Links: ACM Digital Library, Paid-for access through Edinburgh University Library |
 |
Inheritance is not subtyping Cook, Hill and Canning In POPL ’90: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1990. DOI: 10.1145/96709.96721 Links: ACM Digital Library, Paid-for access through Edinburgh University Library |
 |
java.util.Collections.max(…) Java 2 JDK 1.2, 1998 The original release of the Collections classes. Link: Documentation from Sun recorded by the Wayback Machine |
 |
java.util.Collections.max(…) Java 8, 2014 The most recent Collections classes, making use of generics, bounds and wildcards. Link: Documentation from Oracle |
 |
The Computer Language Benchmarks Game Previously the Computer Language Shootout, with its custom “Completely Random and Arbitrary Point System” select-your-own scorecard. Links: The Benchmarks Game; Archives of The Shootout and The Scorecard |
 |
Even Higher-Order Functions for Parsing or: Why would anyone ever want to use a sixth-order function? Chris Okasaki Journal of Functional Programming 8(2):195–199, March 1998 DOI: 10.1017/S0956796898003001 Links: Publisher page, Paid-for access through Edinburgh University Library |
On slide 53 (Encoding Products in System F):
The definition for fst is (abbreviated) Lambda.Lambda.lamda. p X Y (lambda. lambda. x). However, when reducing fst A B (pair A B M N), we get (Lambda Z. lambda f : (A -> B -> Z). f M N) A B (lambda x. lambda y. x). So, we are trying to feed two type arguments – A and B – to an expression expecting only one (the overall return type). Shouldn’t our fst definition then be Lambda.Lambda.lamda. p X (lambda. lambda. x), i.e. without that extra mentioning of the type of the second element of the pair?
Yes, there is an error in this slide (and again in Lecture 5). This was picked up in the lecture by a student, and I thought I had corrected it but evidently not. I have updated slides for both lectures — you may need to reload in your browser to see the corrections.
Thanks for pointing this out.