## 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 language | English |
---|---|

Article number | 3236776 |

Journal | Proceedings of the ACM on Programming Languages |

Volume | 2 |

Issue number | ICFP |

DOIs | |

Publication status | Published - 2018 Sept |

## Keywords

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

## ASJC Scopus subject areas

- Software
- Safety, Risk, Reliability and Quality