Course Topics
TS
On this page, we are going to keep track of topics, papers we're going to study, and so on.
Hindley-Milner: The Type System that is the basis of Haskell
In the first part of the course, we're going to study the type system of Haskell (and ML) in more detail. You're probably familiar with the type rules and the basic inference algorithm, but you might not have read a lot of literature about it. We're going to pick two papers out of the wealth of papers there are:- The Damas-Milner paper: The Original. The standard inference algorithm, described by those who invented it.
- Extending HM type inference algorithms: research in Utrecht about describing HM type inference and variants thereof systematically.
The Lambda Cube
The next part of the course is supposed to focus on a group of typed lambda calculi called the Lambda Cube. We're going to study some specific instances of those lambda calculi, and also literature discussing the Cube itself. I suggest:- Types of Programming Languages: the first of Pierce's books introduces System F and System Fω. The latter is like an explicitly typed variant of Haskell, and as such very interesting for studying extensions to the Haskell type system.
- Barendregt: Introduction to Generalized Type Systems: the paper introducing the Lambda Cube.
Dependent Types
A possible topic for later in the course (which would connect well to the Lambda Cube) is to study dependent types. We could, for example, have a look at:- Simply Easy -- An Implementation of a Dependently Typed Lambda Calculus: A paper describing an implementation of a dependently-typed core language in Haskell.
- View from the Left: a paper about Epigram, a dependently-typed programming language.
Type Classes
Type classes are ubiquitous in Haskell, and with all their extensions, responsible for a sheer endless stream of research papers. We could have a look at type classes, their extensions and implementation: starting from Mark Jones or even Wadler/Blott, we could find our way to advanced type class extensions such as Functional Dependencies and Associated Types.data vs. codata
This seems like an interesting subject to me. The first paper I could find on this topic is: http://www.jucs.org/jucs_10_7/total_functional_programming Any other suggestions? -- JeielSchalkwijk - 14 Oct 2007Your Favourite Topic
If you want to learn about a specific type system extension, propose it. The schedule isn't completely fixed yet, so we can adapt it to cover your interests. Here are more options:- GADTs (also System FC, and possibly associated types)
- ML module system
- ...
As another possible topic, I'd like to suggest "impredicative polymorphism". I know what it means for practical programming, but have no idea what it really means and what its connections with impredicativity in type theory / mathematics / proof assistants are. -- RemiTurk - 08 Sep 2007 Good point. Do you have any paper suggestions? -- AndresLoeh - 19 Sep 2007 Unfortunately, not really. There is of course the boxy types paper, but that's perhaps a bit ghc-specific and in any case rather type inference-specific. Then, the problems with impredicativity are at least briefly talked about in type theoretic books like Type Theory and Functional Programming. And then, err, Wikipedia has something to say on the subject.. -- RemiTurk - 19 Sep 2007 I also think that Boxy Types is maybe a bit too ghc-specific. Thompson book is a good pointer, I wanted to scan that for suitable material anyway. But generally, I'd just say that we focus on whatever we read and revisit this issue whenever it comes up again. -- AndresLoeh - 25 Sep 2007
I'm not sure if it's a suggestion or a plan, but I would really like to study Type Classes, so here's a vote for that! -- ChrisEidhof - 18 Sep 2007 Now that there is a team working on Associated Types, it might be a good idea to study type classes as well. It doesn't connect nicely to the Lambda Cube stuff, but maybe we can do it later. -- AndresLoeh - 19 Sep 2007
Scrap your type applications (PDF) About a variation on System F in which many type applications can be made implicit: System IF. The weird thing is that the same paper used to also contain a description of System QF, which is weaker than F, but has no explicit type applications. Google cache still has this version. But I would prefer to spend more time on dependent types
Ah -- had only you mentioned Barry Jay, I would have recalled this paper ... Yes, that might be a good
candidate for reading.
-- AndresLoeh - 25 Sep 2007