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.
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 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
data vs. codata
This seems like an interesting subject to me. The first paper I could find on this topic is:
Any other suggestions?
- 14 Oct 2007
Your 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
- 05 Sep 2007
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.
- 08 Sep 2007
Good point. Do you have any paper suggestions?
- 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..
- 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.
- 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!
- 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
- 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.
- 25 Sep 2007