Introduction

Andromeda 2 is a proof checker for user-definable dependently-typed theories. It follows the design of LCF-style theorem provers:

• There is an abstract datatype judgement whose values can only be constructed by a nucleus, a small trusted component of the proof checker,

• The user interacts with the nucleus by writing programs in a high-level, statically typed meta-language Andromeda ML (AML).

• Normalization, unification, and other proof development techniques reside outside the trusted nucleus. They are implemented in AML, or in some cases in OCaml.

• Andromeda 2 uses algebraic effects and handlers as a control mechanism for directing proof search.

Developers

• Andrej Bauer
• Gaëtan Gilbert
• Philipp G. Haselwarter
• Anja Petković Komel
• Matija Pretnar
• Chris Stone

A bit of history

Andromeda 1 was first conceived by Andrej Bauer during the Univalent Foundations of Mathematics 2012/13 program at the Institute for Advanced Study. The original idea was to use algebraic effects and handlers as a mechanism for implementing a proof checker for extensional type theory. In 2017 Andrej Bauer and Philipp Haselwarter implemented Andromeda 2, which allowed user-defined type theories, of which extensional type theory was just one example.

In conversations with Vladimir Voevodsky about type theory and its role in formal proof checking, we would sometimes talk about “sending proofs to a far away place where they will check them independently, like Brazil”. Thus, in the beginning the name of the proof checker was Brazil. It later turned out Brazil was not quite far enough. Martin Escardó suggested the name Andromeda. We hope that nobody will claim that our neighboring galaxy is a nearby place.

Support

This material is based upon work supported by the Air Force Office of Scientific Research, Air Force Materiel Command, USAF under Award No. FA9550-14-1-0096. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author(s) and do not necessarily reflect the views of the Air Force Office of Scientific Research, Air Force Materiel Command, USAF.

How to install Andromeda

Andromeda is implemented in OCaml and relies on the OPAM package manager for installation. Please make sure you have a recent working OCaml & OPAM.

Execute the following command to get and install Andromeda:

opam pin add andromeda git+https://github.com/Andromedans/andromeda

How to compile Andromeda

If you would like to compile Andromeda yourself, follow these instructions.

Prerequisites

You need OCaml 4.12 or later, and quite possibly it works with earlier versions, and several OCaml packages, which you can install by running

opam install dune dune-build-info dune-site menhir sedlex

For line-editing in the interactive toplevel, install rlwrap (or ledit) and wrap the invocation yourself: rlwrap ./andromeda.exe.

Compilation

Checkout the Andromeda repository

git clone git@github.com:Andromedans/andromeda.git

or consider forking it if you intend to experiment with it, or contribute to the project.

To build Andromeda, run the command

dune build

in the andromeda folder. This will create the executable ./andromeda.exe. You can also run tests with

dune runtest

If you see no input, the tests passed.

Usage

You may run the compiled executable andromeda.exe. For basic usage and command-line options, run

./andromeda.exe --help

The Andromeda meta-language

Andromeda is a proof assistant designed as a programming language, following the tradition of Robin Milner’s Logic for computable functions (LCF). We call it the Andromeda meta-language (AML).

AML is a functional call-by-value language with algebraic effects and handlers. It is statically typed, with Hindley-Milner-style parametric polymorphism and type inference.

Top-level commands are separated by ;;. The examples in this chapter use ;; where a separator is needed, and a leading # to indicate input typed at the Andromeda toplevel.

We refer to AML expressions as computations to emphasize that they may have effects (such as printing things on the screen or instantiating a meta-variable). Every computation runs in one of two modes: inferring mode, where the computation produces whatever value it determines, or checking mode, where the result must match a given target. For judgement-producing computations the target is a boundary, covered under Boundaries in the object type theory chapter.

Andromeda is a generic proof checker. The user defines their own type theory, with respect to which Andromeda computes derivable judgements. Any judgement computed by Andromeda is guaranteed to be derivable from the inference rules postulated by the user.

While Robin Milner’s LCF and its HOL-style descendants compute judgements in simple type theory, AML supports dependent type theories. This creates a significant overhead in the complexity. While John Harrison could print the HOL Light kernel on a T-shirt, we may need a cape to print the 4000 lines of the Andromeda nucleus.

AML-types

The types in AML are called AML-types to distinguish them from the types appearing in the object type theory. They follow closely the usual Hindley-Milner-style parametric polymorphism, with the addition of judgement (the US spelling judgment is also accepted), boundary, and derivation — the type-theoretic values that the user-defined object theory operates on.

A polymorphic type-scheme is written mlforall α β ... γ, t. AML infers schemas automatically for let-bound values, displaying them on the prompt: fun x -> (x, x) is reported with the schema mlforall α, α → α * α. A binding can also be given a schema explicitly with :>, e.g. let f x :> mlforall α, α → α = x.

AML-type definitions

An AML-type abbreviation may be defined as

mltype foo = t

An AML-type may be parametrized:

mltype foo α β ... γ = t

A disjoint sum is defined as

mltype foo =
  | constr₁ of t₁
  ...
  | constrⱼ of tⱼ

A leading | is optional and the declaration is terminated by ;; or by the next top-level command.

Each constructor takes at most one argument. To pack several values into a constructor, use a tuple: | Pair of α * β. Constructors are namespaced under the current module — foo declared at the top level introduces the bare names constr₁ … constrⱼ. They need not be capitalized but they must be fully applied when used as values.

The empty AML-type is defined with no constructors:

mltype empty = | ;;

An AML-type may be declared abstractly, without any constructors. Such a type can be used wherever a type is expected, but it has no introduction or elimination forms inside AML — values of an abstract type are typically produced by externals. The declaration takes the form mltype NAME or mltype NAME α β ... γ.

Inductive AML-datatypes

A recursive AML-type is declared with mltype rec:

mltype rec t α β ... γ =
  | constr₁ of t₁
  ...
  | constrⱼ of tⱼ

The recursion must be guarded by data constructors, i.e., we only allow inductive definitions. AML-type application is prefix (t α, not α t), so the standard tree datatype reads

mltype rec tree α =
  | Empty
  | Tree of α * tree α * tree α

Mutually recursive types are joined with and:

mltype rec even =
  | Zero
  | SuccE of odd
and odd =
  | SuccO of even

Predefined AML-types

Andromeda binds the following AML-types before any user code runs.

The built-in AML-types, which are reserved keywords and have no user-level constructors:

• mlunit is the unit type whose only value is the empty tuple ()
• mlstring is the type of strings
• judgement is the type of nucleus judgements
• boundary is the type of nucleus boundaries
• derivation is the type of nucleus derivations
• ref t is the type of mutable references to a value of type t

The datatypes pre-defined in the standard library:

• list α is the type of lists, with constructors [] and ::
• ML.option α is the type of optional values, with constructors ML.None and ML.Some
• ML.bool is the type of booleans, with constructors ML.true and ML.false
• ML.order is the type used for comparison of AML values, with constructors ML.less, ML.equal, ML.greater

The judgement, boundary, and derivation AML-types are reflections of the nucleus’s trusted datatypes; their use is covered under the object type theory reference (forthcoming). The ref type and the operations on it appear in Mutable references.

General-purpose programming

AML is a general-purpose programming language which supports the following programming features:

• let-bindings of values
• first-class functions
• (mutually) recursive functions
• datatypes (lists, tuples, and user-definable data types)
• match statements and pattern matching
• operations and handlers
• exceptions
• mutable references
• modules

let-binding

A binding of the form

let x = c₁ in c₂

computes c₁ to a value v, binds x to v, and computes c₂. Thus, whenever x is encountered in c₂, it is replaced by v.

A let-binding may be annotated with an AML-type schema using :>:

# let cow :> mlstring = "cow"
val cow :> mlstring = "cow"

The :> is the AML schema ascription. A binding annotated with : (no >) is read instead as a typing-judgement ascription on a judgement computation, and is covered under the object type theory reference (forthcoming).

It is possible to bind several values simultaneously:

let x₁ = c₁
and x₂ = c₂
 ⋮
and xᵢ = cᵢ in
  c

The bound names x₁, …, xᵢ do not refer to each other, thus:

# let x = "foo"
val x :> mlstring = "foo"
# let y = "bar"
val y :> mlstring = "bar"
# let x = y and y = x in (x, y)
- :> mlstring * mlstring = ("bar", "foo")

You may use patterns in let-bindings, in which case the bound variables should be marked with ?:

# let (?a, ?b) = ("a", "b")
val a :> mlstring = "a"
val b :> mlstring = "b"
# let (ML.Some ?p) = ML.Some ["p"]
val p :> list mlstring = "p" :: []

Functions

An AML function has the form

fun x -> c

Example:

# fun x -> (x, x)
- :> mlforall α, α → α * α = <function>
# (fun x -> (x, x)) "foo"
- :> mlstring * mlstring = ("foo", "foo")

The arguments may be annotated with a type, in which case it is considered a pattern, so any bound variables must be marked with ?:

# fun (?x :> mlstring) -> x
- :> mlstring → mlstring = <function>

An iterated function

fun x₁ -> fun x₂ -> ... -> fun xᵢ -> c

may be written as

fun x₁ x₂ ... xᵢ -> c

A let-binding of the form

let f x₁ ... xᵢ = c

is a shorthand for

let f = (fun x₁ x₂ ... xᵢ -> c)

You may use patterns in function arguments, in which case the bound variables must be marked with ?:

 # let fst = fun (?x, _) -> x
 val fst :> mlforall α β, α * β → α = <function>
 # let snd (_, ?y) = y
 val snd :> mlforall α β, α * β → β = <function>

Recursive functions

Recursive functions can be defined:

let rec f x₁ ... xᵢ = c₁ in
  c₂

is a local recursive function definition. Multiple mutually recursive functions may be defined with

let rec f₁ x₁ x₂ ... = c₁
    and f₂ y₁ y₂ ... = c₂
     ⋮
    and fⱼ z₁ z₂ ... = cⱼ

The inferred type of a recursive function is never polymorphic:

# let rec f x = x
val f :> _α → _α
# f "foo"
- :> mlstring = "foo"
# f
- :> mlstring → mlstring = <function>

To define a polymorphic recursive function, we have to annotate it explicitly:

# let rec f x :> mlforall a, a -> a = x
val f :> mlforall α, α → α

User-defined operators

AML lets you bind names made of symbol characters and use them in prefix or infix position. Such an operator is declared like any other function, except that the operator’s name is enclosed in parentheses on the left-hand side of the let:

# let (|>) x f = f x
val ( |> ) :> mlforall α β, α → (α → β) → β = <function>
# "hello" |> (fun s -> (s, s))
- :> mlstring * mlstring = ("hello", "hello")

At the call site the parentheses are dropped; the operator is written between its arguments (infix) or before its argument (prefix). A prefix operator is declared the same way and applied in prefix position:

# let (~+) x = (x, x)
val ( ~+ ) :> mlforall α, α → α * α = <function>
# ~+ "hi"
- :> mlstring * mlstring = ("hi", "hi")

Precedence and associativity

The precedence and associativity of an operator are determined by its first character. The table below lists the seven operator classes, from lowest precedence to highest:

Characters that may appear after the first one, in any operator, are: ! $ % & * + - . / : < = > ? @ ^ | ~ ×.

The standard library binds |> for forward function application and = for value equality; && and || are bound when the booleans theory is loaded.

Reserved operator tokens

A handful of operator-shaped tokens belong to the language itself and cannot be rebound:

Note also that the standard prelude pre-binds ? as an operation (see the meta-variable section — forthcoming), so you cannot rebind ? on its own while the prelude is loaded; pass --no-prelude on the command line if you really need to.

Sequencing

The sequencing construct

c₁ ; c₂

computes c₁, discards the result, and computes c₂. It is equivalent to

let _ = c₁ in c₂

If c₁ has type other than mlunit, a warning is printed.

Predefined data values

Strings

A string is a sequence of characters delimited by quotes, e.g.

"This string contains forty-two characters."

Its type is mlstring. There are no built-in operations on strings other than printing; equality and comparison are exposed by the standard library via the compare external.

Tuples

A meta-level tuple is written as (c₁, ..., cᵢ). Its type is t₁ * ... * tᵢ where tⱼ is the type of cⱼ. The unit value () has type mlunit.

Optional values

The value ML.None indicates a lack of value and ML.Some c indicates the presence of value c. The type of ML.None is mlforall α, ML.option α; the type of ML.Some c is ML.option t if t is the type of c.

Lists

The empty list is written as []. The list whose head is c₁ and the tail is c₂ is written as c₁ :: c₂. The computation

[c₁; c₂; ... cᵢ]

is shorthand for

c₁ :: (c₂ :: ... (cᵢ :: []))

Note the semicolon separator inside the brackets; commas would build a tuple. A list of type list t must hold values of type t.

match statements and patterns

A match statement is also known as case in some languages and is simulated by successive if-else if-…-else if-else in others. The general form is

match c with
| p₁ -> c₁
| p₂ -> c₂
  ...
| pᵢ -> cᵢ
end

The first clause whose pattern matches c is evaluated. The variables bound in pᵢ are available in cᵢ. If no pattern matches the value, a runtime error is reported.

The leading bar | may be omitted. A pattern may be guarded with a boolean condition:

| pᵢ when bᵢ -> cᵢ

In this case, the value of c has to match pᵢ and the guard bᵢ must evaluate to ML.true. The variables bound in pᵢ are available in both bᵢ and cᵢ.

Example:

# match ["foo"; "bar"; "baz"] with
  | ?x :: (?y :: _) -> ML.Some (y, x)
  | _              -> ML.None
  end
- :> ML.option (mlstring * mlstring) = ML.Some (("bar", "foo"))

The first pattern matches the list, binding x to "foo" and y to "bar".

AML patterns

The patterns that match ordinary AML values are:

Patterns must be linear, i.e., in a pattern each pattern variable ?x may appear at most once.

Judgement and boundary patterns

In addition to the AML patterns above, AML has patterns that destructure the nucleus’s judgements and boundaries. The full story — what judgements and boundaries are, how they arise, and how the four forms relate to the rules of the object type theory — belongs to the object type theory reference (forthcoming). For pattern-matching purposes only, the available forms are:

Write ⁇ (or the ASCII ??) wherever a boundary pattern needs to say “this is a boundary of this kind”. The boundary patterns are useful in operation cases, where the checking-mode boundary comes in after the colon, e.g.

with
  | operation (?) : ML.Some (⁇ : ?t) -> ...
end

binds ?t to the type carried by the term boundary.

Operations and handlers

AML operations and handlers are similar to those of the Coop programming language. They let the user-level code intercept and react to events that arise during evaluation — equality questions, coercion requests, missing information — rather than baking them into the nucleus.

Operations

A new operation is declared by

operation op : t₁ → t₂ → ... → tᵢ → u

where op is the operation name, t₁, …, tᵢ are the types of the operation arguments, and u is its return type. There need not be any arguments, i.e., it is valid to declare

operation op : u

An operation is then invoked with

op c₁ .. cᵢ

where cⱼ must have type tⱼ, and the type of the computation is u.

When an operation is invoked, it propagates outward to the innermost handler that has a matching case for it. The handler decides what value to return; that value is then resumed back into the computation that invoked the operation. Operations are like resumable exceptions — control returns to the point of invocation, unless the handler raises a proper exception instead.

Handlers

A handler value has the form

handler
| case₁
| case₂
...
| caseⱼ
end

where each caseᵢ is an operation case, an exception case, or a value case. The first case that matches is used. If no case matches, the value, exception, or operation propagates outward to the next enclosing handler.

A handler that handles a computation of type t and produces a result of type u has the AML-type t ⇒ u (ASCII synonym: t => u). That is the type printed for handler values, as in val g :> mlstring ⇒ mlstring = <handler>.

Operation cases

An operation case in a handler … end value has the form

| op p₁ ... pᵢ -> c

or the form

| op p₁ ... pᵢ : p -> c

The first form matches an invoked operation op' v₁ ... vᵢ when op equals op' and each vⱼ matches the corresponding pattern pⱼ. The second form additionally matches the checking-mode boundary against p: when the operation was invoked in checking mode with boundary bdry, then ML.Some bdry matches p; in inferring mode, ML.None matches p. (Inferring and checking modes are explained under Boundaries in the object type theory chapter.) The boundary patterns can be used here to destructure the boundary.

When an operation case matches, the body c is evaluated with the pattern variables bound to the corresponding values. The value v produced by c is passed back to the point of operation invocation, unless c itself raises an exception.

Value cases

A value case has the form

| val p -> c

It is used when the handled computation evaluates to a value v without invoking any operation. The first value case whose pattern matches v is used.

If no value case is present in the handler, the trivial case val ?x -> x is assumed. If at least one value case is present but the handled computation evaluates to a value matched by none of them, a runtime error occurs.

Exception cases

An exception case has the form

| raise p -> c

It catches an exception matched by p and evaluates c. An exception is non-resumable, so the value of c becomes the value of the entire with … try … construct.

The handling construct

To actually handle a computation c with a handler h write

with h try c

The notation

try
  c
with
| handler-case₁
...
| handler-caseᵢ
end

is a shorthand for

with
  handler
  | handler-case₁
  ...
  | handler-caseᵢ
  end
try
  c

Several handlers may be stacked on top of each other, for instance

with h₁ try
  ...
  with h₂ try
    ...
    c
    ...

When a computation c invokes an operation, the operation is handled by the innermost enclosing handler that has a matching case for it.

Exceptions

Exception types are declared at the top level. The declaration

exception Exn

introduces a nullary exception, and

exception Exn of t

introduces an exception that carries one piece of data of AML-type t.

An exception is raised with

raise (Exn c)

(or raise Exn for a nullary exception), and caught by an exception case in a handler. Exceptions are non-resumable: when caught, control does not return to the raise site, it stays in the handler’s body.

For example:

# exception StrExn of mlstring
Exception StrExn is declared.
# let g = handler | raise StrExn ?s -> s end
val g :> mlstring ⇒ mlstring = <handler>
# with g try raise (StrExn "msg")
- :> mlstring = "msg"

Top-level handlers

Handlers may also be installed globally with a top-level command:

with
  | operation op₁ p₁₁ ... -> c₁
  ...
  | operation opᵢ pᵢ₁ ... -> cᵢ
end

Note the syntactic difference: at the top level each operation case begins with the keyword operation, while operation cases inside a handler … end value begin directly with the operation’s name. A top-level handler installation replaces whatever handler was previously installed for the named operations. The top-level form accepts operation cases only.

Mutable references

Mutable references are as in OCaml:

• a fresh reference is introduced by ref c where c evaluates to its initial value
• if c evaluates to a reference, its value can be accessed by ! c
• if c evaluates to a reference, its value can be modified by c := c' where c' evaluates to the new value.

The AML-type of a mutable cell holding values of type t is ref t.

Modules

Andromeda has a simple module system for grouping declarations and controlling namespaces. There are four constructs:

Defining a module inline

A submodule may be defined directly in the source:

module M = struct
  let greeting = "hello"
  mltype color = | Red | Green | Blue
end

After this declaration, the names inside M are accessible with dotted qualification: M.greeting, M.Red, M.color. Module names are ordinary identifiers; any identifier may serve as a module name, though by convention modules are capitalised.

require

The toplevel command

require X

looks for a file named X.m31 and processes it as a module. The search path is the directory of the current file followed by any directories supplied via the -I command-line flag. Each file is loaded at most once per session — re-requiring an already-loaded module is a no-op.

The standard library is automatically on the search path unless --no-stdlib is given. The stock prelude is loaded automatically unless --no-prelude is given.

Several modules may be required at once:

require base, eq

include

include M

copies the bindings of module M into the current namespace. The copied bindings remain accessible after the inclusion both unqualified (greeting) and as members of M (M.greeting). Use include when you want the included names to be re-exported as part of the enclosing module.

open

open M

makes the bindings of M accessible without qualification in subsequent code, but does not re-export them. After open M, you write greeting directly; clients of the surrounding module still need M.greeting (unless they too open M).

Qualified paths may have several components: Module.Submodule.name.

Top-level directives

These two commands talk to Andromeda itself: external binds an AML name to a value provided by Andromeda outside AML, and verbosity sets the diagnostic level.

external

The top-level form

external name : schema = "key"

binds name to a value provided by Andromeda outside AML (typically a function written in OCaml). The quoted "key" selects which external value is meant — it must match one of the keys Andromeda exposes. The schema gives the AML-type at which the external is to be used; it is the user’s responsibility to write a schema that matches the external’s actual type.

The standard library uses external to bring in each native value it needs. For instance, it declares printing and comparison this way:

external print : mlforall a, a -> mlunit = "print"
external compare : mlforall a, a -> a -> ML.order = "compare"

and exposes the equality-checker primitives by writing:

mltype checker ;;

external empty_checker : checker
  = "Eqchk.empty_checker" ;;

external add : checker -> derivation -> checker
  = "Eqchk.add" ;;

A binding made by external behaves like any other let-bound value once declared. The full list of available external keys is part of the reference appendix (forthcoming).

verbosity

The top-level directive

verbosity n

sets the diagnostic verbosity to level n. The levels are:

A higher level includes everything at lower levels. The same option can also be set from the shell with the -V n command-line flag.

The object type theory

An object type theory in Andromeda is given by postulating its inference rules with rule declarations; Andromeda itself is generic in this choice. The vocabulary of the object level has three principal kinds of value:

• A judgement, of AML-type judgement, is formal evidence of one of four judgement forms.
• A boundary, of AML-type boundary, is a classifier for judgements, describing the shape of a judgement that is to be constructed.
• A derivation, of AML-type derivation, is a parametric proof-builder: it takes judgements for its formal parameters and produces a judgement of a specified shape. Primitive derivations are introduced at the top level by rule declarations; derived ones are produced by the derive computation.

Every judgement, boundary, and derivation originates in the nucleus, the small trusted component of the implementation. The nucleus admits two kinds of inference rule: those the user has postulated, and a fixed collection of general structural rules — congruence rules, and the reflexivity, symmetry, and transitivity of judgemental equality. From this design follows the central correctness guarantee:

Important

Soundness. Every value of AML-type judgement computed by Andromeda is derivable from the inference rules declared by the user and the built-in structural rules.

Judgements

There are four primitive judgement forms:

Each form asserts a specific kind of well-formedness or judgemental equality; together they make up the entire body of statements that the nucleus can certify.

The type judgement and the term judgement are the object judgements; they assert that something has been constructed. The type equality and the term equality are the equality judgements; they assert that two object judgements identify the same thing.

A judgement records its context. When several judgements are combined — by applying a rule, by appealing to an equality — the nucleus joins their contexts in the result.

The expressions appearing in a judgement are built by applying the inference rules of the object theory, and may additionally contain atoms, meta-variables, and abstractions.

Atoms

An atom is a free variable of the object theory. (We prefer “atom” to “object-level variable” as it is shorter and avoids confusion between different kinds of variables.)

An atom is introduced into a judgement by the fresh construct and discharged from its context by the dual abstract construct. In the body of an abstraction, a bound variable appears as an atom.

Meta-variables

A meta-variable is a named placeholder standing for a yet-to-be-supplied judgement. Every meta-variable carries a boundary that classifies it: a type meta-variable stands for a type, a term meta-variable for a term of a known type, an equational meta-variable for a judgemental equality.

A meta-variable is introduced into a judgement by the meta construct, and most often arises as a formal parameter of a derivation.

Abstractions

An abstraction {x : A} J parametrises a judgement (or a boundary) J over an atom x of type A. (The curly braces do not indicate implicit arguments, as Andromeda has no implicit arguments.) An abstracted judgement is itself of AML-type judgement, and an abstracted boundary of AML-type boundary. Abstractions nest, and binders that share a type may be grouped: {x y z : A} J is the same as {x : A} {y : A} {z : A} J, and {x : A} {y : B{x}} J abstracts over x and y in turn.

An abstraction is instantiated by writing C{e}: if C evaluates to an abstracted judgement {x : A} J and e to a term of type A, then C{e} is the result of instantiating x with e in J. Successive instantiations are written C{e₁, e₂}, peeling off two binders in order. For example, assuming we have a type A and an element a : A, the abstraction {x : A} x instantiated at a gives:

# let f = {x : A} x ;;
val f :> judgement = ⊢ {x : A} x : A
# f {a} ;;
- :> judgement = ⊢ a : A

Boundaries

A boundary specifies the shape of a judgement that is to be constructed. In a computation a boundary expresses a goal to be reached. There are four boundary forms, one for each judgement form:

The ⁇ marker (ASCII ??) stands at the position where the head of the judgement needs to be filled in; the rest of the boundary fixes the data the judgement must agree with.

Boundaries, like judgements, can be abstracted. An abstracted boundary {x : A} B classifies abstracted judgements {x : A} J in which the body J is classified by B.

Boundary ascription :?

The construct c :? B evaluates c in checking mode against the boundary B. If c computes a judgement j that matches B, then j is the result of c :? B. If there is a mismatch, Andromeda triggers the ML.coerce j B operation, giving user code a chance to convert j. A handler may catch ML.coerce B and resume the computation by passing any judgement j' whose boundary is B. Of course, the intended use is that j' be computed from j.

Inference rules

A rule declaration introduces a primitive derivation; the derive computation builds a derived one inside AML.

The rule declaration

A top-level rule declaration has the form

rule NAME premise₁ premise₂ ... premiseₙ : conclusion

where NAME is the rule’s name, each premiseᵢ describes a premise together with its boundary, and conclusion fixes the shape of the resulting judgement. The declaration introduces NAME as a value of AML-type derivation and applies it to its premises by ordinary juxtaposition. For example:

# rule A type ;;
Rule A is postulated.
# A
- :> judgement = ⊢ A type
# rule a : A ;;
Rule a is postulated.
# rule F (x : A) type ;;
Rule F is postulated.
# F
- :> derivation = derive (x : A) → F x type
# F a
- :> judgement = ⊢ F a type

A and a are zero-premise rules and so evaluate directly to the corresponding judgements. F is a one-premise rule and its bare name is the derivation that takes a term of type A to a type judgement; applying it to a yields the judgement ⊢ F a type.

Premises

A premise is enclosed in parentheses and has two presentations. The basic form spells out the boundary explicitly with :?,

(z :? B)

where z names the premise and B is the boundary. The shorthand drops the :? and the ⁇ marker, lets the boundary terminator (type, : T, ≡ … by …) stand for the shape of the boundary, and lifts any local-context prefix out of the boundary parentheses. The two presentations are interchangeable. For each of the four boundary forms:

In the equality shorthand the name sits after by, not before the body, since the body is the equation itself.

A premise may also be abstracted over local atoms by prefixing a local context {x : A} …. In the basic form the local context sits inside the boundary; in the shorthand it is lifted to the front of the premise. The dependent-product formation rule, with one type premise and one type premise indexed by an element of the first, illustrates the contrast:

Tip

(* Basic form throughout *)
rule Π (A :? ⁇ type) (B :? {x : A} ⁇ type) type

(* Shorthand throughout — what one writes in practice *)
rule Π (A type) ({x : A} B type) type

Both declarations produce the same derivation. The J-rule for the identity type carries a deeper local context. Assuming Id and refl have been postulated as

Tip

rule Id (A type) (a : A) (b : A) type ;;
rule refl (A type) (a : A) : Id A a a ;;

the J-rule reads

Tip

rule J
  (A type)
  ({x y : A} {p : Id A x y} C type)
  ({x : A} c : C{x, x, refl A x})
  (a : A)
  (b : A)
  (q : Id A a b)
  : C{a, b, q}

The motive premise ({x y : A} {p : Id A x y} C type) has a three-binder local-context prefix; its basic-form equivalent is (C :? {x y : A} {p : Id A x y} ⁇ type).

Judgement computations in AML

AML offers a small set of computations that construct, transform, or inspect nucleus judgements.

fresh

The computation fresh x : A, generates a previously-unseen atom xᵢ of type A and returns the judgement stating that xᵢ has type A in context xᵢ : A:

# fresh x : A
- :> judgement = x₀ : A ⊢ x₀ : A

AML reports that it computed the judgement x₀ : A ⊢ x₀ : A, whose AML type is judgement. Running the same computation again yields a different atom:

# fresh x : A
- :> judgement = x₁ : A ⊢ x₁ : A

The identifier x in fresh x : A is the display name carried into the atom; the subscript ᵢ is added by the pretty-printer so that atoms which happen to share a display name are still distinguishable on the page.

abstract

The computation abstract a c takes a free atom a and a judgement (or boundary) c, and returns the abstracted judgement {a : T} c, in which a no longer occurs free. A typical session opens with fresh to bring an atom into scope, builds up a judgement that depends on it, and closes with abstract to discharge the atom. Assuming there is a type A and a term constructor f:

# let y = fresh y : A
val y :> judgement = y₀ : A ⊢ y₀ : A
# f y
- :> judgement = y₀ : A ⊢ f y₀ : A
# abstract y (f y)
- :> judgement = ⊢ {y : A} f y : A

The result of the last computation is the abstracted term judgement {y : A} f y : A; its context is now empty, as y has been discharged.

meta

The computation meta x introduces a fresh meta-variable in a checking-mode position. The name x becomes the meta’s display name; successive uses of meta x produce distinct meta-variables, disambiguated in the pretty-printer by subscripts:

# rule A type ;;
Rule A is postulated.
# meta x :? ?? type
- :> judgement = ?x₀ type ⊢ ?x₀ type
# meta x :? (?? : A)
- :> judgement = ?x₁ : A ⊢ ?x₁ : A

derive

The computation

derive premise₁ ... premiseₙ -> body

builds a derived derivation. Each declared premise introduces a fresh meta-variable bound under the premise’s name in the body; the body evaluates to the conclusion judgement. The resulting derivation is applied like a primitive rule, by juxtaposition with its arguments:

# rule A type ;;
Rule A is postulated.
# let id = derive (A type) -> A ;;
val id :> derivation = derive (A type) → A type
# id A
- :> judgement = ⊢ A type

Juxtaposition applies a derivation only when there is at least one argument. A derivation of zero arity is applied with the judgement keyword (the US spelling judgment is also accepted), which is the explicit form of derivation application:

# rule c : A ;;
Rule c is postulated.
# let r = derive -> c ;;
val r :> derivation = derive → c : A
# judgement r
- :> judgement = ⊢ c : A

The keyword accepts further arguments as well: judgement d e₁ … eₙ is equivalent to d e₁ … eₙ whenever the latter parses.

convert

The computation convert e ξ transports a term e of type A along a type equality ξ : A ≡ B to obtain a term of type B. Assuming a postulated equality eq : A ≡ B and a term e : A:

# convert e eq
- :> judgement = ⊢ e : B

congruence

The computation

congruence j₁ j₂ ξ₁ ... ξₖ

proves an equality between two judgements j₁ and j₂ that share the same head, given equality witnesses ξᵢ for each pair of corresponding sub-arguments. The result is an equality judgement relating j₁ to j₂.

rewrite

The computation

rewrite j ξ₁ ... ξₖ

applies the equalities ξᵢ as rewrites inside the judgement j, returning a pair: the equality witness that relates the input to the rewritten judgement, and the rewritten judgement itself.

context

The computation context j yields the list of free atoms on which the judgement j depends, each presented as a term judgement giving the atom and its type:

# rule A type ;;
Rule A is postulated.
# let x = fresh x : A in context x
- :> list judgement = (x₀ : A ⊢ x₀ : A) :: []

occurs

The computation occurs x j tests whether the atom x occurs free in the judgement j. The result is ML.None if x does not appear in j, or ML.Some t where t is the type judgement giving x’s type:

# rule A type ;;
Rule A is postulated.
# let x = fresh x : A in occurs x x
- :> ML.option judgement = ML.Some (⊢ A type)

natural

For a term judgement e : A, the computation natural e returns the type equality B ≡ A, where B is the natural type of e (the type read off e’s head) and A is the type at which e is currently held. When no conversion has intervened the natural type and the current type coincide, and the resulting equality is reflexive:

# rule A type ;;
Rule A is postulated.
# rule a : A ;;
Rule a is postulated.
# natural a
- :> judgement = ⊢ A ≡ A

Judgement and boundary patterns

The judgement and boundary patterns, listed in the AML chapter under Judgement and boundary patterns, destructure nucleus judgements and boundaries by their form. The semantic content of each pattern is:

The linearity requirement

For a derivation to be registered with the equality checker as a rule (see Equality checking below), each of its premise meta-variables must appear exactly once in the head of the conclusion. The checker uses this linearity to recover the premises from the shape of the goal.

Equality checking via the standard library

Andromeda’s nucleus only sees syntactic (α-)equality. Substantive judgemental equality is delegated to user code through the equal_type and coerce operations the runtime triggers when a boundary needs to be matched. The standard library installs handlers for these operations that run an extensible equality checker, configured by adding derivations as equality rules.

The eq module

The eq module exposes the equality checker. Its principal names are add_rule for registering a derivation as a rule, add_locally for scoping a rule to a sub-computation, and normalize_type and normalize_term for driving a judgement toward a normal form. The module also installs the runtime handlers that consult the checker when equal_type or coerce is raised.

Adding rules: eq.add_rule

eq.add_rule drv registers the derivation drv as an equality rule with the global checker. The rule must satisfy the linearity requirement; the checker classifies the rule as either a β-rule or an extensionality rule by inspecting its shape.

Local rules: eq.add_locally

eq.add_locally drv (fun () -> c) adds drv to the checker for the duration of the computation c and retracts it afterwards. This is the idiom for using an equality rule only inside a particular derivation.

Normalisation: eq.normalize_type, eq.normalize_term

eq.normalize_type chk sgn t and eq.normalize_term chk sgn e repeatedly apply the β-rules registered with the checker chk until no rule fires, returning a pair of (the equality witness relating the input to its normal form, the normal-form judgement itself).

β-rules and extensionality rules

The checker accepts two shapes of equality rule.

A β-rule (or computation rule) rewrites a redex. Its conclusion has the form head … ≡ … : T, where the left-hand side’s head is a recognisable constructor and the right-hand side is the redex’s reduct. The β-rule for the dependent product, for instance, reduces app A B (λ A' B' s) a to s{a}.

An extensionality rule equates two terms by exhibiting agreement of their components. Its conclusion has the form x ≡ y : T, where x and y are the last two premises and T constrains the type at which they are compared. Function extensionality — two functions are equal when they agree pointwise — is the standard example.

A worked example: the dependent product

The type former Π takes a type A and a type B indexed by an element of A, and yields a type:

rule Π (A type) ({x : A} B type) type

The introduction λ takes the same two premises plus a body — a term of B{x} parametric in x : A — and yields a term of type Π A B:

rule λ (A type) ({x : A} B type) ({x : A} e : B{x}) : Π A B

The elimination app takes a function s : Π A B and an argument a : A, yielding a term of B{a}:

rule app (A type) ({x : A} B type) (s : Π A B) (a : A) : B{a}

These three rules give the shape of the dependent product; behaviour is supplied by equality rules registered with the checker. The β rule reduces an application of λ to its argument. The full declaration carries extra premises so that the rule applies up to definitional equality of the domain and codomain:

rule Π_β (A type) ({x : A} B type)
         (A' type) ({x : A'} B' type)
         ({x : A'} s : B'{x}) (a : A)
         (A' ≡ A by ξ) ({x : A'} B'{x} ≡ B{convert x ξ} by ζ)
         :?
         (eq.add_locally (derive -> ξ) (fun () ->
           eq.add_locally (derive (x : A') -> ζ{x}) (fun () ->
             app A B (λ A' B' s) a ≡ s{a} : B{a} by ??
           )))
eq.add_rule Π_β

Extensionality says two functions are equal when they agree pointwise:

rule Π_ext (A type) ({x : A} B type)
           (f : Π A B) (g : Π A B)
           ({x : A} app A B f x ≡ app A B g x : B{x})
           : f ≡ g : Π A B
eq.add_rule Π_ext

Once these declarations are in scope, the checker handles β-reduction and function extensionality automatically wherever a boundary is to be matched.

Publications

Papers

• Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone. Design and implementation of the Andromeda proof assistant. 22nd International Conference on Types for Proofs and Programs (TYPES 2016), May 2016, Novi Sad, Serbia.

• Andrej Bauer, Anja Petković Komel. An extensible equality checking algorithm for dependent type theories. Logical Methods in Computer Science, January 19, 2022, Volume 18, Issue 1.

• Andrej Bauer, Philipp G. Haselwarter, Anja Petković Komel. Equality Checking for General Type Theories in Andromeda 2 Mathematical Software – ICMS 2020. Lecture Notes in Computer Science, volume 12097, pages 253–259, Springer.

• Philipp G. Haselwarter, Andrej Bauer. Finitary Type Theories With and Without Contexts. Journal of Automated Reasoning, Volume 67, article number 36, October 2023.

Talks

• Andrej Bauer. Derivations as computations. Invited keynote talk. 24th ACM SIGPLAN International Conference on Functional Programming – ICFP 2019, August 2019, Berlin, Germany. (slides)

• Philipp G. Haselwarter, Andrej Bauer. Type theories without contexts. 27th International Conference on Types for Proofs and Programs, 14–18 June 2021, online. (slides)

• Anja Petković Komel. Equality Checking for Finitary Type Theories HoTTEST Conference 2020, June 18, 2020 (slides)