Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age

Roland Leißa, Marcel Ulrich, Joachim Meyer, Sebastian Hack

TL;DR

This paper presents MImIR, an extensible, higher-order intermediate representation that is a pure type system and, hence, a form of a typed lambda calculus and shows the expressiveness and effectiveness of MImIR in three case studies.

Abstract

Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. Optimizations should understand the primitive operations of the specific application domain and thus happen on that level. Domain-specific languages (DSLs) fulfill these requirements. However, DSL compilers reinvent the wheel over and over again as standard optimizations, code generators, and general infrastructure & boilerplate code must be reimplemented for each DSL compiler. This paper presents MimIR, an extensible, higher-order intermediate representation. At its core, MimIR is a pure type system and, hence, a form of a typed lambda calculus. Developers can declare the signatures of new (domain-specific) operations, called "axioms". An axiom can be the declaration of a function, a type constructor, or any other entity with a possibly polymorphic, polytypic, and/or dependent type. This way, developers can extend MimIR at any low or high level and bundle them in a "plugin". Plugins extend the compiler and take care of optimizing and lowering the plugins' axioms. We show the expressiveness and effectiveness of MimIR in three case studies: Low-level plugins that operate at the same level of abstraction as LLVM, a regular-expression matching plugin, and plugins for linear algebra and automatic differentiation. We show that in all three studies, MimIR produces code that has state-of-the-art performance.

MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age

TL;DR

This paper presents MImIR, an extensible, higher-order intermediate representation that is a pure type system and, hence, a form of a typed lambda calculus and shows the expressiveness and effectiveness of MImIR in three case studies.

Abstract

Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. Optimizations should understand the primitive operations of the specific application domain and thus happen on that level. Domain-specific languages (DSLs) fulfill these requirements. However, DSL compilers reinvent the wheel over and over again as standard optimizations, code generators, and general infrastructure & boilerplate code must be reimplemented for each DSL compiler. This paper presents MimIR, an extensible, higher-order intermediate representation. At its core, MimIR is a pure type system and, hence, a form of a typed lambda calculus. Developers can declare the signatures of new (domain-specific) operations, called "axioms". An axiom can be the declaration of a function, a type constructor, or any other entity with a possibly polymorphic, polytypic, and/or dependent type. This way, developers can extend MimIR at any low or high level and bundle them in a "plugin". Plugins extend the compiler and take care of optimizing and lowering the plugins' axioms. We show the expressiveness and effectiveness of MimIR in three case studies: Low-level plugins that operate at the same level of abstraction as LLVM, a regular-expression matching plugin, and plugins for linear algebra and automatic differentiation. We show that in all three studies, MimIR produces code that has state-of-the-art performance.

Paper Structure

This paper contains 39 sections, 2 theorems, 8 equations, 12 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Contributions
  3. Overview
  4. Plugin Architecture
  5. Plugin Declaration
  6. Types
  7. Normalization
  8. Semantics
  9. Syntax, Typing & Normalization
  10. Preliminaries
  11. Normalization
  12. Substitution
  13. Nat & Idx
  14. Tuples, Packs, Arrays & $\Sigma$-Types
  15. Assignable
  16. ...and 24 more sections

Key Result

lemma 1

If $\hlgamma \vdash {\texttt{\color{ACMBlue}e}} : {\texttt{\color{ACMBlue}T}}$, then e is a value or there exists an e' such that ${\texttt{\color{ACMBlue}e}} \to {\texttt{\color{ACMBlue}e'}}$.

Figures (12)

  • Figure 1: Syntax, $\beta$-Reduction, Typing, & Normalization. ${\texttt{\color{ACMBlue}\ul{e}}}$might not be normalized; ${\texttt{\color{ACMBlue}e}}$is normalized.
  • Figure 2: Simple syntactic sugar
  • Figure 3: Curried functions/continuations
  • Figure 4: Curried function/continuation types
  • Figure 6: Two additions in Mim
  • ...and 7 more figures

Theorems & Definitions (2)

  • lemma 1: Progress
  • lemma 2: Preservation