Home
• Education Page
• Topics
• Schedule
• Projects

• Interesting Links

Center
Master Program
Course Topics

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&omega;. 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?

-- Main.JeielSchalkwijk - 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
   *  ...

-- Main.AndresLoeh - 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.

-- Main.RemiTurk - 08 Sep 2007

Good point. Do you have any paper suggestions?
   
-- Main.AndresLoeh - 19 Sep 2007

Unfortunately, not really. There is of course the [[https://research.microsoft.com/users/simonpj/papers/boxy/ 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 [[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]]. And then, err, [[http://en.wikipedia.org/wiki/Polymorphism_(computer_science)#Predicativity_Restrictions Wikipedia]] has something to say on the subject..

-- Main.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.

-- Main.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!

-- Main.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.

-- Main.AndresLoeh - 19 Sep 2007

---

[[http://research.microsoft.com/users/simonpj/papers/variant-f/qf.pdf 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. [[http://64.233.183.104/search?q=cache:2HZ96RQd2gcJ:https://research.microsoft.com/users/simonpj/papers/variant-f/qf.pdf+%22scrap+your+type+applications%22+QF 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. 

-- Main.AndresLoeh - 25 Sep 2007