This project provides a high-performance implementation of a dependent type theory elaborator, demonstrating advanced techniques for optimizing type checking and elaboration speed. It is targeted at researchers and developers interested in the performance characteristics of dependently typed languages and offers a fast alternative to existing systems like Agda, Coq, and Lean.

How It Works

The core of smalltt is built upon "semantic elaboration" or "normalization-by-evaluation" (NbE), which contrasts with less efficient term substitution methods. It employs "glued evaluation" to balance the need for efficient evaluation during conversion checking with the desire for minimal term sizes during quoting, achieved by lazily controlling top-level definition unfolding. Contextual metavariables are used, where each metavariable abstracts over its scope, and pattern unification handles meta solutions.

Quick Start & Requirements

• Install using stack install or cabal v2-install in the project directory.
• For performance gains, use stack install --flag smalltt:llvm or cabal v2-install -fllvm if LLVM is installed.
• Executable is typically found in $HOME/.local/bin (stack) or $HOME/.cabal/bin (cabal).
• See Basics.stt for introductory examples.

Highlighted Details

• Demonstrates techniques for high-performance elaboration, aiming to outperform existing systems.
• Utilizes "glued evaluation" for optimized quoting and conversion checking.
• Implements contextual metavariables and pattern unification for meta-solutions.
• Features bounded approximate conversion checking with "rigid", "flex", and "full" states.
• Achieves eta-short meta solutions by prioritizing direct meta solutions over eta-expansion.

Maintenance & Community

• This is a demo project, and code/documentation may change.
• Benchmarks are provided comparing smalltt against Agda, Coq, Lean, and Idris 2.

Licensing & Compatibility

• The README does not explicitly state a license.

Limitations & Caveats

• The project is described as a demo and not yet finalized, with potential for changes.
• Some optimizations are missing, and further tuning based on real-world data is needed.
• The current implementation of occurs checking is quadratic on certain benchmarks, though fast enough to be a "non-issue."