11
$\begingroup$

There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.

There are also multiple possible ways to check definitional equality (an essential part of typechecking for a dependently typed language). For normalization, there is traditional step-by-step $\beta$-reductions, using different strategies such as call-by-name, call-by-value, or call-by-need, and similarly using or not using explicit substitutions, and other variations. There is also normalization-by-evaluation, which also has variations such as whether closures are defunctionalized. And an equality-checking algorithm can use normalization in different ways, e.g. it could just normalize both terms all the way (perhaps including $\eta$-expansion or not) and compare the normal forms, or it could traverse them step-by-step mimicking a normalization algorithm and comparing as it goes. It could also try a "short-circuit" comparison of not-fully-normalized terms in hopes of detecting some equalities faster before falling back on full normalization, and I'm sure there are many other variations.

There are lots of interesting theoretical arguments to be made about which combinations of these choices are better (and for which purposes); for instance, one "sweet spot" theoretically seems to be normalization-by-evaluation with De Bruijn indices for unevaluated "terms" and De Bruijn levels for evaluated "values".

But what I want to know right now is what implementations of real-world dependently typed proof assistants actually do, today, to represent bound variables and check equality.

Specifically, I want to know what combinations of choices have actually proven to scale effectively and efficiently in practice. Thus, by "real-world" I mean a proof assistant that's used by significant numbers of people for large-scale formalization projects. I'm particularly interested in Coq, Agda, and Lean, since I have the most experience with them, but I would also be interested in answers addressing other proof assistants that fit those criteria.

$\endgroup$
6
  • 2
    $\begingroup$ Getting tired of programming those induces by hand, eh? $\endgroup$ Commented Jun 3 at 6:56
  • 1
    $\begingroup$ @AndrejBauer No, I'm not having any trouble with indices. I'm using intrinsically well-scoped indices for terms (and levels for values), which is a dream. But I am having trouble with efficiency, so I mainly want to know what designs for equality-checking have proven to be practically optimizable, and whether they depend on particular choices for representing binders. $\endgroup$ Commented Jun 3 at 14:23
  • 1
    $\begingroup$ Intrinsically well-scoped? Are you implementing things in a dependently typed language? $\endgroup$ Commented Jun 3 at 15:27
  • 1
    $\begingroup$ @AndrejBauer Not a fully dependently typed language; I'm using GADTs and type-level natural numbers in OCaml. $\endgroup$ Commented Jun 3 at 18:22
  • 1
    $\begingroup$ Do you know what is making it slow? Have you tried profiling it? (I take it we're talking about narya, which looks very interesting BTW!) $\endgroup$ Commented Jun 3 at 20:20

5 Answers 5

8
$\begingroup$

Variables

λΠ uses the Bindlib library, and so do several other systems, see the paper Abstract Representation of Binders in OCaml using the Bindlib Library and package documentation. I have recently started using and I am happy with it. For a minimalistic example of its use see my educational implementation of Spartan Type Theory.

Some nice features:

  • Boiler-plate code that needs to be written upfront, so that the library can connect with your syntax, is very straightforward.
  • The OCaml type checker prevents you from accidentally using a term with an "exposed" bound variable. (That's a real saver.)
  • Checking whether a variable occurs in a term is $O(n)$ where $n$ is the number of variables occurring in the term.
  • Substitution is lightning fast.

Here's a quick recap of how it works. Bindlib provides an abstract type of variables 'a var, where 'a is the type that such variables will be substituted for (typically a type of terms). When you build a new term, you don't actually use your own datatype myTerm but rather the Bindlib-wrapped type myTerm box so that Bindlib can manage all the variable magic (for example, it keeps track of the variables appearing in a term). Once you're done you can unbox : myTerm box -> myTerm the Bindlib-wrapped term to obtain an actual term.

Equality checking

Spartan Type Theory implements the Harper-Stone style equality checking algorithm that work very well in the presence of extensionality rules – these are equivalant to $\eta$-rules, but allow more principled use. The price you pay is typed equality. See section 3.4 of An extensible equality-checking algorithm for dependent type theories (written with Anja Petković Komel) and its improvement Generic bidirectional typing for dependent type theories by Thiago Felicissimo.

However, I would not recommend learning equality checking algorithms from Spartan Type Theory. A much better source is Andras Kovacs' Elaboration zoo, which shows how to implement not only bare equality checking, but also holes, implicit arguments, meta-variables, and other technology that any implementation eventually has to deal with.

$\endgroup$
13
  • 2
    $\begingroup$ The type of variables is abstract, but if you'd like to look under the hood, here it is. $\endgroup$ Commented Jun 3 at 15:16
  • 5
    $\begingroup$ The Elaboration zoo is not to be dismissed so easily. Andras is one of the best experts on implementation techniques, and he's essentially demonstrating state-of-the-art. For example, his zoo shows how to do an improved version of implict arguments from his ICFP 2020 paper Elaboration with first-class implicit function types. I don't think anyone can do better than that at the moment. $\endgroup$ Commented Jun 3 at 15:25
  • 3
    $\begingroup$ But it is, because the elaboration zoo is very close to what is implemented in practice, and in fact if you're going to dig through Agda or Coq, you'd be well advised to first look at the elaboration zoo. That's what I am answering. $\endgroup$ Commented Jun 3 at 19:01
  • 3
    $\begingroup$ After I read through the elaboration zoo, will I know what is done in Agda and in Coq? If not, I don't regard it as an answer. I want to avoid digging through their source code myself; I assumed that there was someone in the world who's already familiar with that source code and would be able to tell me what it does. $\endgroup$ Commented Jun 3 at 19:38
  • 3
    $\begingroup$ Thanks! Equality checking is what I really wanted to know about, so I hope an actual expert shows up. I'm not sure why you're so exercised about my asking what actual proof assistants do currently; it seems to me like a perfectly reasonable thing to want to know. I didn't say I was planning to copy them. I've read plenty about the "right" or "future" way to do things; is it so ridiculous to want to be able to compare that in an informed way with what people have done in the past? $\endgroup$ Commented Jun 3 at 20:17
7
$\begingroup$

Idris 2 is self-hosted and as such it can use dependent types when specifying the operations on its own intermediate representations.

Variables

The core language is well-scoped by construction which seems to be a sweet spot. It uses lists of names as its notion of scopes because Nats are not appropriate notions of scope: nothing looks more 1+1+n (a non-empty scope extended with a fresh variable) than 1+1+n (a non-empty scope weakened by inserting a variable between the most local one and the rest).

Ideally we should be using snoclists of names (various attempts at a new core do) because in inference rules contexts grow on the right and it's mentally draining to always "think backwards" in the implementation.

We use Quantitative Type Theory to statically enforce that the only thing that remains after compilation of a De Bruijn index is a GMP-style integer:

||| A variable in a scope is a name, a De Bruijn index,
||| and a proof that the name is at that position in the scope.
||| Everything but the De Bruijn index is erased.
public export
record Var {0 a : Type} (vars : List a) where
  constructor MkVar
  {varIdx : Nat}
  {0 varNm : a}
  0 varPrf : IsVar varNm varIdx vars

Equality checking

It's based on normalisation by evaluation. The new core follows Andras Kovacs' glued evaluator approach so as to avoid unfolding definitions more than needed. We have a sprinkle of phantom types to be able to state explicitly whether a function assumes that a value has been head-normalised already thus reducing silly mistakes whereby you build the glued value but forget to force the computation and end up with an unexpected suspended application.

$\endgroup$
5
  • $\begingroup$ Do you use the same representation for terms and values in NbE? And can you give a reference for the "glued evaluator approach"? $\endgroup$ Commented Jun 3 at 14:29
  • 1
    $\begingroup$ The best description of "glued evaluation" I've found so far is github.com/AndrasKovacs/…. Is there anything more written about it than that? $\endgroup$ Commented Jun 3 at 20:11
  • 1
    $\begingroup$ I might be missing something obvious here, but: why is it called "glued evaluation"? $\endgroup$ Commented Jun 3 at 23:54
  • 1
    $\begingroup$ @DavidYoung computing two things at the same time is reminiscent of Artin gluing, a technique for proving certain metatheoretic properties (see here or here). $\endgroup$ Commented Jun 4 at 6:56
  • 1
    $\begingroup$ @MikeShulman here's another intro to it: andraskovacs.github.io/pdfs/wits24prez.pdf $\endgroup$
    – ice1000
    Commented Jun 5 at 20:35
6
$\begingroup$

Since you asked about Lean, it uses De Bruijn indices and naive/explicit substitution for bound variables, unique names/locally nameless for free variables, and call by name with caching. The substitution and abstraction procedures implement two optimizations, first that they work on sequences, substituting or abstracting more than one variable at a time. Second, expressions have some extra data that prevents these procedures from traversing into subterms that do not have bound variables which need to be replaced or free variables that need to be extracted.

De Bruijn levels are more performant than unique names, but they're more difficult to use in the part of the kernel that checks inductive specifications and generates elimination rules.

Free variables also carry type information around with them, so there's no separate typing context.

Lean's procedure for checking equality does try to short-circuit without fully reducing, mainly by unfolding definitions and theorems lazily. It also keeps a cache of when two constants (references to declarations, like definitions that haven't been unfolded) were tested for definitional equality but failed, and that turns out to actually be pretty important for performance. Proof irrelevance is also part of the kernel, which is sort of a short circuit. The kernel does try eta expansion, and some other stuff.

One thing Lean's kernel does everywhere it can that is a "real world" thing (in that it's pretty important for performance, but doesn't appear in textbook treatments) is extend operations to spines/telescopes where possible, like applying N arguments to a lambda with M binders, then re-folding any arguments that are left over.

I wrote a short book about lean's kernel that has some more detailed information about the reduction, inference, and equality procedures (chapters 8-10), and some of the earlier chapters talk about the expression and variable representations, it's hosted here: https://ammkrn.github.io/type_checking_in_lean4/

I'm not sure how Lean's kernel compares to similar systems in terms of performance (in my opinion it's really difficult to find and compare on similar work loads since a "realistic work load" is specific to what people write in the vernacular of that particular language), but there are at least two people working on faster implementations as personal projects.

$\endgroup$
2
  • $\begingroup$ Are one of those two people Mario with his Lean4Lean project? I remember him saying that one goal of that project was to prove the kernel correct and then optimize it, showing the kernel is still correct after each optimization. $\endgroup$
    – Jason Rute
    Commented Jun 4 at 1:15
  • $\begingroup$ @JasonRute Yes, but "working on" is maybe too strong, he just mentioned he's looking into alternative implementations that are more performant. I don't know whether it will be integrated into lean4lean, but the last time I checked l4l adheres very closely to the C++ kernel. $\endgroup$ Commented Jun 4 at 1:21
6
$\begingroup$

Core term definition

In the latest version of Aya, we use locally nameless approach where names are represented by Java object identity (see this), and bound variables are integers (see this).

Bound variables in core term

Closures (sub-terms that bind variables), have two implementations: using locally nameless (so instantiation is the standard locally nameless instantiation), and using JVM HOAS JIT compilation (e.g. compile the closure into Java function and instantiation is just calling that Java function), and the source code is here. When you finish type checking a file, it compiles all definitions into Java functions and will call these functions to instantiate them, instead of traversing terms recursively to perform the substitution, which we expect to be more efficient.

Equality

The conversion checking is bidirectional (see code), so for introduction forms we have the type information, this allows us to better handle metavariable resolution and unit type η-laws.

$\endgroup$
4
$\begingroup$

Agda

Variables in Agda are represented as de Bruijn indices, and there is a type of explicit substitutions that is used in many places throughout the typechecker.

Reduction is done by a lazy abstract machine. Pattern matching definitions are represented as case trees for more efficient evaluation.

Equality checking alternates between three phases:

  1. A fast syntactic comparison that does not do any reduction but dismisses equations if both sides are identical.
  2. A type-directed phase that applies simplifications based on the type of the equation (in particular dealing with irrelevance and eta-equality).
  3. A syntax-directed phase that computes the weak-head normal form of both sides and recurses into the arguments (which then start again in phase 1).

By default, Agda will never compare arguments of functions that are not in whnf in order to ensure uniqueness of metavariable solutions. However, you can change this behavior by using the --lossy-unification flag (or by using the upcoming INJECTIVE_FOR_INFERENCE pragma.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.