smalltt

Demo project for several techniques for high-performance elaboration with dependent types.

It is a complete rewrite of the old smalltt version which I wrote mostly in 2018-2019.

Table of Contents

• Overview
• Installation
• Language overview
• Design
  • Basics
    • NbE vs. naive evaluation
  • Contextual metavariables
  • Glued evaluation
    • On hash consing
  • Strict vs. lazy evaluation
  • Approximate conversion checking
  • Paired values
  • Eta-short meta solutions
  • Meta solution checking and quotation
  • Meta freezing and approximate occurs checking
• GHC-specific optimizations
  • Runtime system options
  • Custom exceptions
  • Data structures and libraries
• Benchmarks
  • Elaboration speed
  • Elaboration asymptotics
  • Raw conversion checking
  • Raw evaluation and normalization

Overview

This project serves as a demo for several techniques for high-performance elaboration with dependent types. I also include some benchmarks, which are intended to be as similar as possible across Agda, Lean, Coq, Idris 2 and smalltt.

You can skip to benchmarks if that's what you're after.

Smalltt is fast, however:

• Smalltt is not as nearly as fast as it could possibly be. A lot of tuning based on real-world benchmarking data is missing here, because there isn't any real-world code for smalltt besides the benchmarks that I wrote. A bunch of plausible optimizations are also missing.
• The primary motivation is to demonstrate designs that can plausibly scale up to feature-complete languages, still yield great performance there, and naturally support a lot more optimization and tuning than what's included here.

This project is not yet finalized. Code and documentation alike may be subject to change, cleanup, extension, or perhaps complete rewrite.

Installation

First, clone or download this repository.

Using stack:

• Install stack.
• Run stack install in the smalltt directory. If you have LLVM installed, use stack install --flag smalltt:llvm instead, that gives some performance boost.

Using cabal:

• Install cabal
• Run cabal v2-update.
• Run cabal v2-install in the smalltt directory. If you have LLVM, use cabal v2-install -fllvm instead.

Also make sure that the executable is on the PATH. On Linux-es, the stack install directory is $HOME/.local/bin, and the cabal one is $HOME/.cabal/bin.

Installation gets you the smalltt executable. You can find usage information after starting smalltt.

Language overview

Smalltt is a minimal dependent type theory implementation. Features:

• Type-in-type.
• Dependent functions.
• Agda-style implicit functions with named implicit arguments.
• Basic pattern unification.
• A distinguished top-level scope and local let-definitions.
• An executable which can load a single file at once, and lets us query top-level definitions in several ways.

See Basics.stt for introductory examples.

Design

Basics

The core design is based on Coquand's algorithm. This is sometimes called "elaboration with normalization-by-evaluation", or "semantic elaboration". This is becoming the de facto standard design of dependently typed elaboration nowadays, but it is in fact the preferred design for elaboration with any type system which includes binders and substitution in types. It is explained in detail in

• https://davidchristiansen.dk/tutorials/nbe/
• https://github.com/AndrasKovacs/elaboration-zoo

I give a short review. Dependent type checking involves execution of arbitrary functional programs at compile time. For executing functional programs, the standard practice (used in virtually all functional languages) is to have

1. Immutable program code, which may be machine code or interpreted code.
2. Runtime objects, consisting of constructors and closures.

The basic idea is to use the above setup during elaboration, with some extensions.

The elaborator takes as input raw syntax, and outputs core syntax, which corresponds to immutable program code. When necessary, we evaluate core syntax into semantic values (or values in short), which correspond to runtime objects, and indeed they represent function values as closures.

Evaluation and runtime values have to support a somewhat richer feature set than what is typical in functional languages. They must support open evaluation, that is, evaluation of programs which may contain free variables. This makes it possible to evaluate code under binders. In such code, free variables cause evaluation to get stuck. There are special values corresponding to stuck computations, which are called neutral values.

Neutral values make it possible to convert runtime values back to core syntax. This is called quoting. Quoting is used in elaboration whenever we need to serialize or store values. For example, since elaboration outputs core syntax, whenever we need to fill a hole in raw syntax, we plug the hole by converting a value to a core term by quoting.

Normalization by evaluation (NbE) means normalizing terms by first evaluating then quoting them. The kind of normal forms that we get can vary depending on the details of evaluation and quoting. In particular, it is not mandatory that NbE yields beta-normal terms.

Moreover, values support conversion checking. Type equality checking is required in pretty much any type checker. In dependently typed languages, types may include arbitrary programs, and equality checking becomes beta-eta conversion checking of values. At its simplest, this is implemented by recursively walking values. The "open" evaluation makes it possible to get inside closures during conversion checking, so we can check if two functions have beta-eta-convertible bodies.

NbE vs. naive evaluation

Elaboration with NbE can be contrasted to elaboration with "naive" evaluation. In this style, compile-time evaluation is performed by term substitution, which is far less efficient than NbE. In some implementations, naive substitution is still used because of its perceived simplicity. However, my experience is that NbE is significantly simpler to implement, and also easier to correctly implement, than capture-avoiding substitution. Furthermore, any attempt to use naive substitution in type checking necessitates additional optimizations, which add more complexity.

For example, Lean uses naive substitution in its kernel, but to recover acceptable performance it has to add extra machinery (memoization, free variable annotations on terms for skipping traversals during substitutions). This ends up being slower and more complicated than a straightforward NbE implementation.

In summary, term substitution should be avoided whenever possible in elaboration implementations. Sometimes it's necessary, but AFAIK only for more niche purposes in more feature-rich systems, and not in performance-critical tasks. Smalltt uses no substitution operation whatsoever, and we can go pretty far without one.

(Remark: cubical type theories are notorious for requiring substitution from the get go. It's an open research problem how to get rid of naive substitution there).

Contextual metavariables

Smalltt uses contextual metavariables. This means that every metavariable is a function which abstracts over the bound variables in its scope. Take the following surface code.

id : (A : U) → A → A
 = λ A x. x

id2 : (A : U) → A → A
 = λ A x. id _ x

When the elaborator hits the hole in id2, it fills it with a fresh metavariable which abstracts over A and x. The elaboration output is:

id : (A : U) → A → A
  = λ A x. x

?0 = λ A x. A

id2 : (A : U) → A → A
  = λ A x. id (?0 A x) x

Note that ?0 is a fresh top-level definition and the hole gets plugged with it. Smalltt's particular flavor of contextual metavariables puts metas in mutual top-level blocks in the elaboration output. Other setups are possible, including elaborating solved metas to local let-definitions, but those are significantly more complicated to implement.

Also, smalltt uses basic pattern unification for producing meta solutions. See this for a tutorial on the basics of contextual metavariables and pattern unification.

Smalltt does not try very hard to optimize the representation of contextual metas, it just reuses plain lambdas to abstract over scopes. For potential optimizations, see this Coq discussion: https://github.com/coq/coq/issues/12526. As a result, basic operations involving metas are usually linear in the size of the local scope. My benchmarking showed that this is not a significant bottleneck in realistic user-written code, and we don't really have machine-generated code (e.g. by tactics) that could introduce pathologically sized local scopes.

Glued evaluation

The most basic NbE setup is not adequate for performance. The problem is that we need different features in conversion checking and in quoting:

• In basic conversion checking, we want to evaluate as efficiently as possible.
• In quoting, we want t