Intersection types and computational effects

9 years 10 months ago
Intersection types and computational effects
We show that standard formulations of intersection type systems are unsound in the presence of computational effects, and propose a solution similar to the value restriction for polymorphism adopted in the revised definition of Standard ML. It differs in that it is not tied to let-expressions and requires an additional weakening of the usual subtyping rules. We also present a bi-directional type-checking algorithm for the resulting language that does not require an excessive amount of type annotations and illustrate it through some examples. We further show that the type assignment system can be extended to incorporate parametric polymorphism. Taken together, we see our system and associated type-checking algorithm as a significant step towards the introduction of intersection types into realistic programming languages. The added expressive power would allow many more properties of programs to be stated by the programmer and statically verified by a compiler. Categories and Subje...
Rowan Davies, Frank Pfenning
Added 01 Aug 2010
Updated 01 Aug 2010
Type Conference
Year 2000
Where ICFP
Authors Rowan Davies, Frank Pfenning
Comments (0)