Elaborating evaluation-order polymorphism

ICFP 2015 (Vancouver, August–September 2015); arXiv:1504.07680 [cs.PL]

Joshua Dunfield

Abstract

We classify programming languages according to evaluation order: each language fixes one evaluation order as the default, making it transparent to program in that evaluation order, and troublesome to program in the other.

This paper develops a type system that is impartial with respect to evaluation order. Evaluation order is implicit in terms, and explicit in types, with by-value and by-name versions of type connectives. A form of intersection type quantifies over evaluation orders, describing code that is agnostic over (that is, polymorphic in) evaluation order. By allowing such generic code, programs can express the by-value and by-name versions of a computation without code duplication.

We also formulate a type system that only has by-value connectives, plus a type that generalizes the difference between by-value and by-name connectives: it is either a suspension (by name) or a “no-op” (by value). We show a straightforward encoding of the impartial type system into the more economical one. Then we define an elaboration from the economical language to a call-by-value semantics, and prove that elaborating a well-typed source program, where evaluation order is implicit, produces a well-typed target program where evaluation order is explicit. We also prove a simulation between evaluation of the target program and reductions (either by-value or by-name) in the source program.

Finally, we prove that typing, elaboration, and evaluation are faithful to the type annotations given in the source program: if the programmer only writes by-value types, no by-name reductions can occur at run time.

Conference slides and video (YouTube)

Final version (June 2015)

BibTeX entry

  @InProceedings{Dunfield15:evaluation,
    author =    {Joshua Dunfield},
    title =     {Elaborating Evaluation-Order Polymorphism},
    year =      {2015},
    booktitle = {Int'l Conf. Functional Programming},
    month =     aug,
    note =      {\href{http://arxiv.org/abs/1504.07680}{arXiv:{\tt 1504.07680 [cs.PL]}}}
  }
  

Note

I submitted this paper to the arXiv, and granted the arXiv a distribution licence. The arXiv is efficiently managed and 100% open-access; the ACM Digital Library is neither. I consider the arXiv version to be canonical.
all papers
Joshua Dunfield