[PL-sem-jr] papers on intersection types

[Felix S Klock]

PL Jr Squad-

Your mission, if you choose to accept it, is to skim over the following  
papers and read the last one.

"Intersection Type Assignment Systems" -- Steffen van Bakel
http://www.doc.ic.ac.uk/~svb/Research/Papers/TCS95.pdf
"Lambda Calculi with Types" -- Henk Barendregt
ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps

These papers were the source for my initial overview of the Torino  
systems.  Barendregt's presentation is great, but he only presents his  
one system.  van Bakel's is readable, but perhaps only after you've  
grokked Barendregt.

"What are principal typings and what are they good for?" -- Trevor Jim
http://www.church-project.org/reports/Jim:MIT-LCS-1995-532.html

This (of course) is the source for the discussion about Principal Types  
versus Principal Typings.  Go here to actually see the subtyping and  
type-derivation rules for P_2 (Jim's system of Rank-2 Intersection  
Types for typing ML programs), and more concrete explanations of how  
one can use Principal Typings for effectively typing REC expressions,  
LETREC expressions, code entered at the repl, code in separate modules  
without type annotations, etc.

"Design of the Programming Language Forsythe" -- John C. Reynolds
ftp://reports.adm.cs.cmu.edu/usr/anon/1996/CMU-CS-96-146.ps.gz

Self explanatory.  See some real wild ideas on how to do things  
differently in a language.  (I actually like the hack of adopting  
intersection types for records, but I'm not as big a fan of the other  
conflations of intersection types).

"Intersection Types and Computational Effects" -- Rowan Davies, Frank  
Pfenning
http://www.cs.cmu.edu/~rwh/courses/refinements/papers/DaviesPfenning00/ 
icfp00.pdf

I didn't present this paper, but its worth reading.  Essentially its  
about how to combine intersection types and ref types (mutable cells).   
  Interestingly, they get around the semi-obvious soundness issues with  
adding mutation by adopting the same solution that Wright and Felleisen  
proposed: put a value restriction on the expressions that can be  
assigned an intersection type.

The paper is both extremely well written and full of content.  One  
issue I have with it is that the authors say that their system lacks  
principal types (and do not mention principal typings); this seems odd  
and I can't find more discussion of why.  But maybe its obvious once  
you look at it carefully.

-Felix

----
"Damn, my wife was right.  White people really
do have ventriloquist dummies"  -www.redmeat.com