Associated Types

Added the final presentation for our project, click here.

-- MaaikeGerritsen? - 07 Nov 2007

---

Yesterday (Tuesday, Oct 16) we have mostly discussed the typing rules of FC (Figures 2 & 3).

Our current aim is

• To understand what each rule does
• To get rid of as many rules as possible:
  • We don't do ADT's, let-in and toplevel values, so Data, Case, Let, Alt and Pgm can go.
  • We don't want function-kinds, so e.g. TyApp, Comp, Left and Right can be scrapped. (Of course, we might still find out that removing function-kinds causes Terrible Things to happen, so we should watch out for that)

Something we realized only yesterday is that there also exists coercions between kinds (in particular, other coercions), so not only do we have coercions like a ~ Int, but also e.g. (a ~ Int) ~ (Int ~ a)

Finally, don't forget to take a quick look at the type family example at the bottom of this page.

---

Today we had another meeting and discussed what we were going to write about. We came to the following conclusion:

Our paper in one line: From System F(omega) to type families

The paper will consist of three parts:

• An introduction to type families
  • Example driven
  • explain type families and give a motivation
  • show what it can be used for
  • give a syntax for type families
  • explain equality constraints and show why we need them
• Show type rules for System F with Coercions
  • Start with system F and add type rules for coercion
  • introduce calculus to translate example
  • show the connection between type families and Fc
• Conclusion

I discovered that I cannot create a repository from home so I will create one on thursday.

-- MaaikeGerritsen? - 09 Oct 2007

Setup for the presentation for thursday:

• start with class definition without data keyword
• start with explanation of associated datatypes
• give motivation for associated datatypes (self-optimising libraries)
• talk about interface abstraction -> bridge to type synonyms
• give an example of functional dependencies
• give an example of type synonyms
• talk about equality constraints of type synonyms
• Towards Open Type Functions for Haskell
• talk about type systems
• GHC Bug

-- MaaikeGerritsen? - 02 Oct 2007

Today we had another meeting with Atze and Andres about our project. We decided that the first step towards the goal of this project is to understand what Associated Types are all about and being to explain this to someone else. So our plan of action for now is to read some important papers which Remi will list. We will then meet coming Tuesday (October 2nd) to set up an explanation between the three of us and prepare a presentation of about half an hour. Then next Thursday (October 4th) we will explain to the group what Associated Types are about.

After this first step there are three possibilities to successfully conclude this project.

• Write a tutorial style paper explaining about Associated Types
• Create a prototype for Associated Types
• Implement Associated Types in EHC

The last one will probably be impossible to do. It would be great if we could accomplish the first and second point, but I think that it would be wisest to first start writing the paper and see how far we get with that.

-- MaaikeGerritsen? - 25 Sep 2007

The list of papers for Tuesday (2-10): Those two papers we should really understand in detail.

• Associated Types with Class
• Associated Type Synonyms

The next four perhaps in slightly less detail.

• Towards Open Type Functions for Haskell This paper is the latest (draft...) paper about associated types / type families / index types / type functions. The described system is the most general, but perhaps not the one we're going to work on. (Although I'd really like to..)

The next papers are all about Constraint Handling Rules & Type Class Extensions. Nothing Associated Types-specific, but important if we're going to look into a prototype.

• A Theory of Overloading
• Theory and Practice of Constraint Handling Rules
• Constraints for Type Class Extensions The master thesis of Gerrit v/d Geest. Besides his thesis itself, there is also a prototype implementation. Our practical work may turn out to be extending his prototype.

-- RemiTurk - 25 Sep 2007

---

First, a very short summary/glossary (please correct me if I'm wrong):

• Associated Datatypes: You can put datatypes in a typeclass
• Associated Type Synonyms: You can put type synonyms in a typeclass
• Associated Types: May mean one or both of the above.
• Type Families or Type Functions: You don't actually need to put them in a typeclass. (If that sounds cryptic, read the papers and improve this sentence )

Some links to more information about Associated Types:

• The Haskell Wiki page on Type Families/Associated Types in GHC
• Associated Types with Class The original paper about Associated Datatypes.
• Associated Type Synonyms The original paper about Associated Type Synonyms.
• System F with Type Equality Coercions System F is one of the intermediate languages of GHC. System FC is an extension in which Functional Dependencies, GADTs and Type Families can be expressed. System FC is probably not very relevant to our project: The "corresponding" intermediate EHC language is untyped.
• Towards Open Type Functions for Haskell About Type Families.
• Constraints for Type Class Extensions The master thesis and code of Gerrit van den Geest, in which he talks about type classes, functional dependencies (related to associated types), CHRs and EHC.
• A Theory of Qualified Types I'm not sure what exactly qualified types have to do with associated types, but IIRC Atze said they are important. See also Qualified Types: Theory and Practice
• Type Classes with Functional Dependencies (PostScript)

-- RemiTurk - 06 Sep 2007

The Associated Types project is accepted in principle. The only thing we're worried about is that a group size of 3 usually makes it a bit difficult to distribute work in such a way that all participants are represented well. After the initial phase, we should reevaluate your interests and try hard to find "subprojects" for each of you, to ensure that everyone has something to do and no one feels lost.

Members of this project, please add yourself to this page.

-- AndresLoeh - 06 Sep 2007

Members

• RemiTurk
• MaaikeGerritsen?
• XavierPardonnet

---

For those who want to experiment with associated types, I have compiled GHC 6.8.20070907 on one of the linux machines. This is a pre-release version, so expect it to contain bugs. It can be "installed" and run as follows:

parrot:~% cd /tmp && tar xjf ~rturk/pub/ghc-6.8.tar.bz2 
parrot:/tmp% /tmp/ghc-6.8/bin/ghci -XTypeFamilies 
GHCi, version 6.8.20070907: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude>

Of course, only one user at a time can install it in /tmp/ghc-6.8, and /tmp seems to cleaned partially quite often, so there might be trouble on some machines. Try another linux machine in that case..

---

If you want to install a type family GHC snapshot yourself, this is how it works: Download a binary GHC snapshot for your architecture from either STABLE or HEAD. For example, if you want 6.9.20071027 for i386:

wget http://www.haskell.org/ghc/dist/current/dist/ghc-6.9.20071027-i386-unknown-linux.tar.bz2
tar xjf ghc-6.9.20071027-i386-unknown-linux.tar.bz2
cd ghc-6.9.20071027
./configure --prefix=/tmp/wherever-you-want-to-install-it
make install
/tmp/wherever-you-want-to-install-it/bin/ghci

Be happy.

---

Email

Remi

(map concat $ sequence $ ap (flip replicate) length ["rturk", "@", "science", ".", "uva", ".", "nl"]) !! 22861

Maaike

mggerrit

Xavier

pardonne