AbstractsComputer Science

Researchers have studied how to type check self-applicable programs. For example, papers by Rendel, Ostermann, and Hofer, and by Jay and Palsberg have shown how to design two kinds of polymorphically typed self-interpreters. In this paper we present the first polymorphically typed self-optimizer. In contrast to a self-interpreter that often can implement each construct by itself, a self-optimizer may replace a subterm with a rather different subterm, which complicates type checking.Our language has combinators, a variant of Mitchell's subtyping, proof terms that help match types, and a novel approach to type check self-application. Via syntactic sugar, we define a surface syntax with decidable type inference. Our implementation has type checked and run our examples.