Intensional Effect Polymorphism

By: Yuheng Long, Yu David Liu, and Hridesh Rajan

Abstract

Type-and-effect systems are a powerful tool for program construction and verification. We describe intensional effect polymorphism, a new foundation for effect systems that integrates static and dynamic effect checking. Our system allows the effect of polymorphic code to be intensionally inspected through a lightweight notion of dynamic typing. When coupled with parametric polymorphism, the powerful system utilizes runtime information to enable precise effect reasoning, while at the same time retains strong type safety guarantees. We build our ideas on top of an imperative core calculus with regions. The technical innovations of our design include a relational notion of effect checking, the use of bounded existential types to capture the subtle interactions between static typing and dynamic typing, and a differential alignment strategy to achieve efficiency in dynamic typing. We demonstrate the applications of intensional effect polymorphism in concurrent programming, memoization, security and UI access.

ACM Reference

Long, Y. et al. 2015. Intensional Effect Polymorphism. 29th European Conference on Object-Oriented Programming, ECOOP, Prague, Czech Republic (2015), 346–370.

BibTeX Reference

@inproceedings{LongLiuRajan2015,
  author = {Yuheng Long and Yu David Liu and Hridesh Rajan},
  title = {Intensional Effect Polymorphism},
  booktitle = {29th European Conference on Object-Oriented Programming, ECOOP, Prague, Czech Republic},
  volume = {37},
  series = {LIPIcs},
  pages = {346--370},
  year = {2015},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  editor = {John Tang Boyland},
  doi = {10.4230/LIPICS.ECOOP.2015.346},
  abstract = {
  Type-and-effect systems are a powerful tool for program construction and
  verification. We describe intensional effect polymorphism, a new foundation
  for effect systems that integrates static and dynamic effect checking. Our
  system allows the effect of polymorphic code to be intensionally inspected
  through a lightweight notion of dynamic typing. When coupled with parametric
  polymorphism, the powerful system utilizes runtime information to enable
  precise effect reasoning, while at the same time retains strong type safety
  guarantees. We build our ideas on top of an imperative core calculus with
  regions. The technical innovations of our design include a relational notion
  of effect checking, the use of bounded existential types to capture the subtle
  interactions between static typing and dynamic typing, and a differential
  alignment strategy to achieve efficiency in dynamic typing. We demonstrate the
  applications of intensional effect polymorphism in concurrent programming,
  memoization, security and UI access.},
}