Intersection types and computational effects

13 years 9 months ago

Download www.cs.cmu.edu

We show that standard formulations of intersection type systems are unsound in the presence of computational eﬀects, and propose a solution similar to the value restriction for polymorphism adopted in the revised deﬁnition of Standard ML. It diﬀers 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 signiﬁcant 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 veriﬁed by a compiler. Categories and Subje...

Rowan Davies, Frank Pfenning

Real-time Traffic