Finitary polymorphism for optimizing type-directed compilation

Research output: Contribution to journalArticlepeer-review

Abstract

We develop a type-theoretical method for optimizing type directed compilation of polymorphic languages, implement the method in SML#, which is a full-scale compiler of Standard ML extended with several advanced features that require type-passing operational semantics, and report its effectiveness through performance evaluation. For this purpose, we first define a predicative second-order lambda calculus with finitary polymorphism, where each type abstraction is explicitly constrained to a finite type universe, and establishes the type soundness with respect to a type-passing operational semantics. Different from a calculus with stratified type universes, type universes of the calculus are terms that represent a finite set of instance types. We then develop a universe reconstruction algorithm that takes a term of the standard second-order lambda calculus, checks if the term is typable with finitary polymorphism, and, if typable, constructs a term in the calculus of finitary polymorphism. Based on these results, we present a type-based optimization method for polymorphic functions. Since our formalism is based on the second-order lambda calculus, it can be used to optimize various polymorphic languages. We implement the optimization method for native (tag-free) data representation and record polymorphism, and evaluate its effectiveness through benchmarks. The evaluation shows that 83.79% of type passing abstractions are eliminated, and achieves the average of 15.28% speed-up of compiled code.

Original languageEnglish
Article number3236776
JournalProceedings of the ACM on Programming Languages
Volume2
Issue numberICFP
DOIs
Publication statusPublished - 2018 Sep

Keywords

  • Compiler Optimization
  • Finitary Polymorphism
  • Second-Order Lambda Calculus
  • SML#
  • Type-Directed Compilation

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint

Dive into the research topics of 'Finitary polymorphism for optimizing type-directed compilation'. Together they form a unique fingerprint.

Cite this