View on GitHub

Andromeda 1

Type theory with equality reflection

$\newcommand{\G}{\Gamma}$ $\newcommand{\D}{\Delta}$ $\newcommand{\tyA}{A}$ $\newcommand{\tyB}{B}$ $\newcommand{\x}{x}$ $\newcommand{\y}{y}$ $\newcommand{\z}{z}$ $\newcommand{\e}{e}$ $\newcommand{\bnf}{\ \mathrel{ {\colon}{\colon}{=}}\ }$ $\newcommand{\bnfor}{\ \mid\ \ }$ $\newcommand{\ctxempty}{\bullet}$ $\newcommand{\ctxextend}[3]{#1,\, #2\, {\colon}\, #3}$ $\newcommand{\Type}{\mathsf{Type}} % The type of all types$ $\newcommand{\Prod}[2]{\mathop{\textstyle\prod_{(#1 {\colon} #2)}}}$ $\newcommand{\lam}[3]{\lambda #1 {\colon} #2.{#3}\,.\,}$ $\newcommand{\app}[5]{#1\mathbin{@^{#2{\colon}#3.#4}} #5}$ $\newcommand{\abst}[2]{[#1 \,.\, #2]}$ $\newcommand{\ascribe}[2]{#1 \,{\colon}\, #2}$ $\newcommand{\JuEqual}[3]{\mathsf{Eq}_{ #1 }( #2, #3 )}$ $\newcommand{\juRefl}[1]{\mathsf{refl}_{#1}\ }$ $\newcommand{\isctx}[1]{#1\ \mathsf{ctx}}$ $\newcommand{\istype}[2]{\isterm{#1}{#2}{\Type}}$ $\newcommand{\isterm}[3]{#1 \vdash\,#2\,:\,#3}$ $\newcommand{\eqctx}[2]{#1 \equiv_{\mathsf{ctx}} #2}$ $\newcommand{\eqtype}[3]{\eqterm{#1}{#2}{#3}{\Type}}$ $\newcommand{\eqterm}[4]{#1 \vdash #2 \equiv #3 : #4}$ $\newcommand{\infer}[2]{\frac{\displaystyle #1}{\displaystyle #2}}$ $\newcommand{\subst}[3]{#1[#3/#2]}$

Table of contents:

About 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).

Andromeda computes typing judgments of the form $\isterm{\G}{\e}{\tyA}$ (“Under assumptions $\G$ term $\e$ has type $\tyA$”), but only the ones that are derivable in type theory with equality reflection. This is known as soundness of AML. Completeness of AML states that every derivable judgment is computed by some program. Neither property has actually been proved yet, we are working on it.

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

While Robin Milner’s LCF and its HOL-style descendants compute judgments in simple type theory, AML computes judgments in dependent type theory. This creates a significant overhead in the complexity of the system and so while John Harisson is able to print the HOL Light kernel on a T-shirt, it may take a super-hero’s cape to print the 1800 lines of Andromeda nucleus.

The constructs of the language are divided into computations which evaluate to values and may emit operations, and top-level commands which have side effects (such as binding a variable to a value) and must be self-contained with regards to operations. An Andromeda program is a list of top-level commands, each containing some computations.

It is important to distinguish the expressions that are evaluated by AML from the expressions of underlying type theory. We refer to AML expressions as computations to emphasize that Andromeda computes their values and that the computations may have effects (such as printing things on the screen). We refer to the expressions of the type theory as (type-theoretic) terms.

ML-types

The AML types are called ML-types in order to be distinguished from the type-theoretic types. They follow closely the usual ML-style parametric polymorphism.

ML-Type definitions

An ML-type abbreviation may be defined as

mltype foo = ...

An ML-type may be parametrized:

mltype foo α β ... γ = ...

A disjoint sum ML-type is defined as

mltype foo =
  | Constructor₁ of t₁₁ and ... and t₁ᵢ
  ...
  | Constructorⱼ of tⱼ₁ and ... and tⱼᵢ
end

The arguments to constructors are written in curried form, e.g., if we have

mltype color = Red | Green | Blue end
mltype cow =
  | Horn of color and color * color
  | Tail of color and color and color

then we write Horn Red (Green, Blue) and Tail Red Green Blue. Data constructors must be fully applied.

The empty ML-type is defined as

type empty = end

Inductive ML-datatypes

A recursive ML-type may be defined as

mltype rec t α β ... γ = ...

The recursion must be guarded by data constructors, i.e., we only allow inductive definitions. E.g., the ML-type of binary trees can be defined as

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

Predefined ML-types

The following types are predefined by Andromeda:

General-purpose programming

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

Note: the match statement is part of the meta-language and is not available in the underlying type theory (where we would have to postulate suitable eliminators instead). It is a mechanism for analyzing terms and other values at the meta-level.

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.

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"
x is defined.
# let y = "bar"
y is defined.
# do let x = y and y = x in (x, y)
("bar", "foo")
Functions

A meta-level function is not to be confused with a $λ$-abstraction in the underlying type theory. A meta-level function has the form

fun x => c

Example:

# do fun x => (x, x)
<function>
# do (fun x => (x, x)) "foo"
("foo", "foo")

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)

A let-binding of the form

let f x₁ ... xᵢ : t = c

is a shorthand for

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

where c : t is type ascription.

Sequencing

The sequencing construct

c₁ ; c₂

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

let _ = c₁ in c₂

except for warning when c₁ has type other than mlunit.

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ⱼ

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 at present no facilities to manipulate strings in AML other than printing.

Tuples

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

Optional values

The value None indicates a lack of value and Some c indicates the presence of value c. The type of None is ∀ α, option α and the type of Some v is 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ᵢ :: []))

At present, due to lack of meta-level types, lists are heterogeneous in the sense that they may contain values of different shapes.

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 bar | may be omitted.

First c is computed to a value v which is matched in order against the patterns p₁, …, pᵢ. If the first matching pattern is pⱼ, by which we mean that it has the shape described by the pattern pⱼ, then the corresponding cⱼ is computed. The pattern pⱼ may bind variables in cⱼ to give cⱼ access to various parts of v.

If no pattern matches v then an error is reported.

Example:

match ["foo","bar","baz"] with
| [] => []
| ?x :: (?y :: _) => (y, x)
end

computes to ("bar", "foo") because the second pattern matches the list and binds x to "foo" and y to "bar".

General patterns

The general patterns are:

_ match any value
?x match any value and bind it to x
p as ?x match according to pattern p and also bind the value to x
x match a value if it equals the value of x
⊢ j match a judgment $\isterm{\G}{\e}{\tyA}$ according to the judgment pattern j, see below
⊢ j₁ : j₂ match a judgment $\isterm{\G}{\e}{\tyA}$ with j₁ and $\isterm{\G}{\tyA}{\Type}$ with j₂
Tag p₁ ... pᵢ match a data tag
[] match the empty list
p₁ :: p₂ match the head and the tail of a non-empty list
[p₁, ..., pᵢ] match the elements of the list
(p₁, ..., pᵢ) match the elements of a tuple

Patterns need not be linear, i.e., a pattern variable ?x may appear several times in which case the corresponding values must be equal. Thus in AML we can compare two values for equality with

match (c₁, c₂) with
| (?x, ?x) => "equal"
| _ => "not equal"
end

Note that a pattern may refer to let-bound values by their name:

# let a = "foo"
a is defined.
# do match ("foo", "foo", "bar") with (a, ?y, ?z) => (y,z) end
("foo", "bar")

In the above match statement the pattern refers to a whose values is "foo".

Judgment patterns

A judgment pattern matches a judgment $\isterm{\G}{\e}{\tyA}$ as follows:

_ match any term
?x match any term and bind it to x
x match the value of x
Type match a universe
∏ (?x : j₁), j₂ match a product (see matching under binders)
∏ (x : j₁), j₂ match a product but not the bound variable
j₁ j₂ match an application
λ (?x : j₁), j₂ match a λ-abstraction
λ (x : j₁), j₂ match a λ-abstraction, but not the bound variable
λ ?x, j shorthand for λ (?x : _), j
j₁ ≡ j₂ match an equality type
refl j match a reflexivity term
_atom ?x match a free variable and bind its natural judgment to x
_constant ?x match a constant and bind its natural judgment to x
Matching under binders

When matching a judgment $\isterm{\G}{∏ (x : A) B}{\Type}$ with a pattern ∏ (y : j₁), j₂, a fresh variable $y₁$ is produced so that we may match $\isterm{\G, y₁ : A}{B}{\Type}$ with j₂.

Patterns which match under a binder have two forms:

Operations and handlers

The AML operations and handlers are similar to those of the Eff programming language. We first explain the syntax and give several examples below.

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.

An operation is then invoked with

op c₁ .. cᵢ

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

One way to think of an operation is as a generalized resumable exception: when an operation is invoked it “propagates” outward to the innermost handler that handles it. The handler may then perform an arbitrary computation, and using yield it may also resume the execution at the point at which the operation was invoked.

Handlers

We can think of a handler as a generalized exception handler, except that it handles one or more operations, as well as values (computations which do not invoke an operation).

A handler has the form

handler
| op-case₁
| op-case₂
...
| op-caseᵢ
| val-case
...
| val-case
| finally-clause
...
| finally-clause
end

where op-case are operation cases, val-case is the value case and finally-clause is the finally clause.

The operation cases

An operation case 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 matches an invoked operation op' v₁ ... vᵢ when op equals op', each vⱼ matches the corresponding pⱼ and if the operation was invoked in checking mode at type t, Some t matches p, otherwise None matches p.

When an operation case matches the corresponding computation c is computed, with the pattern variables appearing in the patterns bound to the corresponding values.

When an operation is invoked it has an associated delimited continuation which is the execution point at which the operation was invoked. The computation c of the handler case may restart the continuation with

yield c'

This will compute c' to a value v which is then passed to the continuation. This will have the effect of resuming computation at the point in which the operation was invoked.

The value cases

A value case has the form

| val ?p => c

It is used when the handler handles a computation that did not invoke a computation but rather computed to a value v. In this case the value cases are matched against the value and the first one that matches is used.

If no value case is present in the handler, it is considered to be the trivial case val ?x => x.

If at least one value case is present, but the handled computation evaluates to a value which is matched by none of them, a runtime error will occur.

The finally case

A finally case has the form

| finally ?p => c

It is used at the very end of handling, after the final value has been computed through handling by operation and value cases. The first finally case that matches is used.

As with value cases, no finally case is equivalent to a trivial case, and non-exhaustive matching results in a runtime error.

The handling construct

To actually handle a computation c with a handler h write

with h handle c

The notation

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

is a shorthand for

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

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

with h₁ handle
  ...
  with h₂ handle
    ...
    c
    ...

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

Example

To show what sort of thing you can do with a handler we implement a feature which allows us to place arbitrary holes in terms. We will use constructs that we have not yet described, in particular

operation Hole 0

let rec prodify xs t =
  match xs with
    | [] => t
    | (|- ?x : ?u) :: ?xs =>
        let t' = forall (y : u), (t where x = y) in
        prodify xs t'
  end

let rec apply head es =
  match es with
    | [] => head
    | ?e :: ?es => (apply head es) e
  end

let hole_filler =
  handler
    Hole : ?t =>
      let xs = hypotheses in
      let t' = prodify xs t in
      assume hole : t' in 
      yield (apply hole xs)
  end

First we declare a nullary operation Hole. Then we define two auxiliary functions that compute iterated products and applications:

# constant A B : Type
Constant A is declared.
Constant B is declared.
# let a = assume a : A in a
a is defined.
# let b = assume b : B in b
b is defined.
# constant F : A -> B -> Type
Constant F is declared.
# do prodify [a, b] (F a b)
⊢ Π (y : B) (y0 : A), F y0 y : Type
# do apply F [b, a]
a₁₀ : A, b₁₁ : B ⊢ F a₁₀ b₁₁ : Type

Now we can use the hole_filler handler to temporarily assume existence of a term by writing Hole anywhere in a term:

# constant A : Type
Constant A is declared.
# constant F : A → Type
Constant F is declared.
# constant G : ∏ (a : A), F a → Type
Constant G is declared.
# do with hole_filler handle λ (a : A), G a Hole
hole₁₆ : Π (y : A), F y
⊢ λ (a : A), G a (hole₁₆ a) : A → Type

Andromeda evaluated G a Hole as follows: it first found out that G is a constant of type ∏ (a : A), F a → Type. Then it evaluated its second argument a in checking mode at type A which evaluated to a : A ⊢ a : A. Then it evaluated the operation Hole in checking mode at type F a. At this point the handler hole_filler handled the operation. It created a new assumption hole₁₆ of type Π (y : A), F y, applied it to a and yield-ed it back. The result was then a λ-abstraction, as displayed.

Here is another, simpler example:

# do with hole_filler handle λ (X : Type) (f : X → X), f Hole
hole₂₂ : Π (y : Type), (y → y) → y 
⊢ λ (X : Type) (f : X → X), f (hole₂₂ X f)
  : Π (X : Type), (X → X) → X

In this case hole_filler created a new assumption hole₂₂ of the displayed type.

Mutable references

Mutable references are as in OCaml:

Dynamic variables

Dynamic variables can be declared only at the top-level, by

dynamic x = c

where c evaluates to the initial value. The current value is accessed with simply x.

Dynamic variables can be updated by the following construct:

now x = c in c'

Here x will evaluate to the result of c when it is used in c', including through function application and operation handling

let f _ = x in
now x = v in f ()

and

handle
  now x = v in getx
with
  getx => yield x
end

both evaluate to v regardless of the previous value of x.

#include_once "<file>"

Include the given file if it has not been included yet.

verbosity <n>

Set the verbosity level. The levels are:

Judgment computations

There is no way in Andromeda to create a bare type-theoretic term $\e$, only a complete typing judgment $\isterm{\G}{\e}{\tyA}$. Even those computations that look like terms actually compute judgments. For instance, if c₁ computes to

and c₂ computes to

then the “application” c₁ c₂ computes to

where $\G \bowtie \D$ is the join of contexts $\G$ and $\D$, satisfying the property that $\G \bowtie \D$ contains both $\G$ and $\D$ (the two contexts $\G$ and $\D$ may be incompatible, in which case Andromeda reports an error).

Even though Andromeda always computes an entire judgment $\isterm{\G}{\e}{\tyA}$ it is useful to think of it as just a term $\e$ with a known type $\tyA$ and assumptions $\G$ which Andromeda is kindly keeping track of.

Inferring and checking mode

A judgment is computed in one of two modes, the inferring or the checking mode.

In the inferring mode the judgment that is being computed is unrestrained.

In checking mode there is a given type $\tyA$ (actually a judgment $\istype{\G}{\tyA}$) and the judgment that is being computed must have the form $\isterm{\D}{\e}{\tyA}$. In other words, the type is prescribed in advanced. For example, an equality type

c₁ ≡ c₂

proceeds as follows:

  1. Compute c₁ in inferring mode to obtain a judgment $\isterm{\G}{\e}{\tyA}$.
  2. Compute c₂ in checking mode at type $\tyA$.

Equality checking

The nucleus and AML only know about syntactic equality (also known as α-equality), and delegate all other equality checks to the user level via a handlers mechanism. There are several situations in which AML triggers an operation that requires the user to provide evidence of an equality (see the section on equality type for information on how to generate evidence of equality).

Operation equal

When AML requires evidence of an equality e₁ ≡ e₂ at type A it triggers the operation equal e₁ e₂. The user provided handler must yield

Operation as_prod

When AML requires evidence that a type A is a dependent product it triggers the operation as_prod A. The user provided handler must yield

Operation as_eq

When AML requires evidence that a type A is an equality type it triggers the operation as_eq A. The user provided handler must yield

Operation coerce

AML evaluates an inferring judgment computation c in checking mode at type B as follows:

The user provided handler must yield a value of type coercible, as follows:

Operation coerce_fun

AML evaluates an application c₁ c₂ as follows:

The user provided handler must yield a value of type coercible as follows:

The universe

The computation

Type

computes the judgment $\istype{}{\Type}$ which is valid by the rule ty-type. Example:

# do Type
⊢ Type : Type

Having Type in Type is unsatisfactory because it renders the type theory inconsistent in the sense that every type is inhabited. We consider this to be a temporary feature of the system that simplifies development. In the future there will be a (user-definable) universe mechanism.

Constants

At the toplevel a new constant a (axiom) of type A may be declared with

constant a : A

Several constants of the same type may be declared with

constant a₁ a₂ ... aᵢ : A

A primitive type T is declared with

constant T : Type

Assumptions

If computation c₁ computes to judgment $\istype{\G}{\tyA}$ then

assume x : c₁ in c₂

binds x to $\isterm{\ctxextend{\G}{\x’}{\tyA}}{\x’}{\tyA}$, then it evaluates c₂. The judgment is valid by rule ctx-var and rule ctx-extend. Example:

# constant A : Type
Constant A is declared.
# constant B : A → Type
Constant B is declared.
# do assume a : A in B a
a₁₁ : A ⊢ B a₁₁ : Type

The judgment that was generated is $\istype{a_{11} \colon A}{\app{B}{x}{A}{\Type}{a_{11}}}$, but Andromeda is not showing the typing annotations. Every time assume is evaluated it generates a fresh variable $\x’$ that has never been seen before:

# do assume a : A in B a
a₁₂ : A ⊢ B a₁₂ : Type
# do assume x : A in B a
a₁₃ : A ⊢ B a₁₃ : Type

If we make several assumptions but then use only some of them, the context will contain those that are actually needed:

# constant A : Type
Constant A is declared.
# constant f : A → A → A
Constant f is declared.
# do assume a : A in (assume b : A in (assume c : A in f a c))
a₁₄ : A, c₁₆ : A ⊢ f a₁₄ c₁₆ : A

Substitution

We can get rid of an assumption with a substitution

c₁ where x = c₂

which replaces in c₁ the assumption bound to x with the judgment that computed by c₂, as follows:

# constant A : Type
Constant A is declared.
# constant a : A
Constant a is declared.
# constant f : A → A
Constant f is declared.
# let x = (assume x : A in x)
x is defined.
# do x
x₁₂ : A ⊢ x₁₂ : A
# let b = f x
b is defined.
# do b
x₁₂ : A ⊢ f x₁₂ : A
# do b where x = a
⊢ f a : A

The idiom let x = assume x : A in x is a common one and it serves as a way of introducing a new fresh variable of a given type. There is no reason to use x both in let and in assume, we could write let z = assume y : A in y but then z would be bound to something like y₄₂ which is perhaps a bit counter-intuitive.

If we compute a term without first storing the assumed variables

# let d = assume y : A in f y
d is defined.
# do d
y₁₃ : A ⊢ f y₁₃ : A

then it is a bit harder to get our hands on y₁₃, but is still doable using context, see below.

Product

A product is computed with

∏ (x : c₁), c₂

An iterated product may be computed with

∏ (x₁₁ ... x₁ⱼ : c₁) ... (xᵢ₁ .... xᵢⱼ : cᵢ), c

Instead of the character ∏ you may also use Π, ∀ or forall.

A non-dependent product is written as

c₁ → c₂

The arrow → associates to the right so that c₁ → c₂ → c₃ is equivalent to c₁ → (c₂ → c₃). Instead of → you can also write ->.

λ-abstraction

A λ-abstraction is computed with

λ (x : c₁), c₂

An iterated λ-abstraction is computed with

λ (x₁₁ ... x₁ⱼ : c₁) ... (xᵢ₁ .... xᵢⱼ : cᵢ), c

In checking mode the types of the bound variables may be omitted, so we can write

λ x₁ x₂ ... xᵢ, c

We can also mix bound variables with and without typing annotations.

Instead of the character λ you may use lambda.

Application

An application is computed with

c₁ c₂

Application associates to the left so that c₁ c₂ c₃ is the same as (c₁ c₂) c₃.

Equality type

The equality type is computed with

c₁ ≡ c₂

Instead of the character ≡ you may use ==. There are a number of constructors for generating elements of the equality types, as follows.

Reflexivity

The reflexivity term is computed with

refl c

If c evaluates to $\isterm{\G}{\e}{\tyA}$ then refl c evaluates to $\isterm{\G}{\juRefl{\tyA} \e}{\JuEqual{\tyA}{\e}{\e}}$.

Reduction

The rule prod-beta is available through

beta_step x A B e₁ e₂

where:

If this is the case, then the computation evaluates to a term of equality type witnessing the fact that

Congruences

The following computations generate evidence for congruence rules. Each one corresponds to an inference rule.

congr_prod (rule cong-prod)

Assuming

the computation

congr_prod x ξ ζ

evaluates to evidence of $\eqtype{\G}{\Prod{\x}{\tyA_1}{\tyA_2}}{\Prod{\x}{\tyB_1}{\tyB_2}}$.

congr_apply (rule congr-apply)

Assuming

the computation

congr_apply x η θ ξ ζ

evaluates to evidence of $\eqterm{\G}{(\app{\e_1}{\x}{\tyA_1}{\tyA_2}{\e_2})}{(\app{\e’_1}{\x}{\tyB_1}{\tyB_2}{\e’_2})}{\subst{\tyA_2}{\x}{\e_2}}$.

congr_lambda (rule congr-lambda)

Assuming

the computation

congr_apply x η θ ξ

evaluates to evidence of $\eqterm{\G}{(\lam{\x}{\tyA_1}{\tyA_2}{\e_1})} {(\lam{\x}{\tyB_1}{\tyB_2}{\e_2})} {\Prod{\x}{\tyA_1}{\tyA_2}}$.

congr_eq (rule congr-eq)

Assuming

the computation

congr_eq η θ ξ

evaluates to evidence of $\eqtype{\G}{\JuEqual{\tyA}{\e_1}{\e_2}}{\JuEqual{\tyB}{\e’_1}{\e’_2}}$.

congr_refl (rule congr-refl)

Assuming

the computation

congr_refl η θ

evaluates to evidence of $\eqterm{\G}{\juRefl{\tyA} \e_1}{\juRefl{\tyB} \e_2}{\JuEqual{\tyA}{\e_1}{\e_1}}$.

Extensionality

Extensionality rules such as function extensionality and uniqueness of identity proofs are not built-in. They may be defined at user level, which indeed they are, see the standard library.

For instance, function extensionality may be axiomatized as

constant funext :
  ∏ (A : Type) (B : A → Type) (f g : ∏ (x : A), B x),
    (∏ (x : A), f x ≡ g x) → f ≡ g

The constant funext can then be used by the standard equality checking algorithm (implemented in the standard library) as an η-rule:

now etas = add_eta funext

Type ascription

Type ascription

c₁ : c₂

first computes c₂, which must evaluate to a type $\istype{\G}{\tyA}$. It then computes c₁ in checking mode at type $\tyA$ thereby guaranteeing that the result will be a judgment of the form $\isterm{\D}{\e}{\tyA}$.

Context and occurs check

The computation

context c

computes c to a judgment $\isterm{\G}{\e}{\tyA}$ and gives the list of all assumptions in $\Gamma$. Example:

# constant A : Type
Constant A is declared.
# constant f : A -> A -> Type
Constant f is declared.
# let b = assume x : A in assume y : A in f x y
b is defined.
# do context b
[(y₁₃ : A ⊢ y₁₃ : A), (x₁₂ : A ⊢ x₁₂ : A)]

The computation

occurs x c

computes x to a judgment $\isterm{\D}{\x}{A}$ and c to a judgment $\isterm{\G}{\e}{\tyA}$ such that $x$ is a variable. It evaluates to None if $x$ does not occur in $\G$, and to Some U if $x$ occurs in $\G$ as an assumption of type U.

# constant A : Type
Constant A is declared.
# constant f : A -> A -> A
Constant f is declared.
# let x = assume x : A in x
x is defined.
# do occurs x (f x x)
Some (⊢ A : Type)
# do occurs x f
None

Hypotheses

In AML computations happen inside products and λ-abstractions, i.e., under binders. It is sometimes important to get the list of the binders. This is done with

hypotheses

Example:

# constant A : Type
Constant A is declared.
# constant F : A → Type
Constant F is declared.
# do ∏ (a : A), F ((λ (x : A), (print hypotheses; x)) a)
[(x₁₄ : A ⊢ x₁₄ : A), (a₁₃ : A ⊢ a₁₃ : A)]
⊢ Π (a : A), F ((λ (x : A), x) a) : Type

Here hypotheses returned the list [(x₁₄ : A ⊢ x₁₄ : A), (a₁₃ : A ⊢ a₁₃ : A)] which was printed, after which ⊢ Π (a : A), F ((λ (x : A), x) a) : Type was computed as the result.

The handling of operations invoked under a binder is considered to be computed under that binder:

# do handle ∏ (a : A), Hole with Hole => hypotheses end
[(a₁₃ : A ⊢ a₁₃ : A)]

Externals

Externals provide a way to call certain OCaml functions. Each function has a name like "print" and is invoked with

external "print"

The name print is bound to the external "print" in the standard library.

The available externals are:

"print" A function taking one value and printing it to the standard output
"time" TODO describe time
"config" A function allowing dynamic modification of some options
"exit" Exit Andromeda ML

The "config" external can be invoked with the following options:

"ascii" Future printing only uses ASCII characters
"no-ascii" Future printing uses UTF-8 characters such as ∏ (default)
"debruijn" Print De Bruijn indices of bound variables in terms
"no-debruijn" Do not print De Bruijn indices of bound variables in terms (default)
"annotate" Print typing annotations (partially implemented)
"no-annotate" Do not print typing annotations (default)
"dependencies" Print dependency information in contexts and terms
"no-dependencies" Do not print dependency information

The arguments to external and external "config" are case sensitive.

Toplevel commands

An Andromeda program is a stream of top-level commands.

Toplevel let binding

The top-level can bind variables to values and define recursive functions like inside computations:

let x = c
and y = c'

and

let rec f x = c
and g y = c'
Toplevel dynamic variables

The top-level can create new dynamic variables

dynamic x = c

and update them for the rest of the program

now x = c
Declarations

The top-level can create new basic values:

Do command

At the toplevel the do c construct computes c:

do c

You cannot just write c because that would create ambiguities. For instance,

let x = c₁
c₂

could mean let x = c₁ c₂ or

let x = c₁
do c₂

We could do without do if we requires that toplevel computations be terminated with ;; a la OCaml. We do not have a strong opinion about this particular syntactic detail.

Fail command

The construct

fail c

is the “opposite” of do c in the sense that it will succeed only if c reports an error. This is useful for testing AML.

If c has side effects they are canceled:

# let x = ref None
x is defined.
# fail x := Some (); None None
The command failed with error:
File "?", line 2, characters 20-23: Runtime error
  cannot apply a data tag
# do !x
None
Toplevel handlers

A global handler may be installed at the toplevel with

handle
| op-case₁
| op-case₂
...
| op-caseᵢ
end

Top-level handlers may only be simple callbacks: the cases may not contain patterns (to avoid confusion, as new cases replace old ones completely) and for case op ?x => c, yield may not appear in c. Instead the result of c is passed to the continuation.

Thus a top-level operation case op ?x => c is equivalent to a general handler case op ?x => yield c.

Include

#include "<file>" includes the given file.

#include_once "<file>" includes the given file if it has not been included yet.

The path is relative to the current file.

Verbosity

#verbosity <n> sets the verbosity level. The levels are:

Help

#help prints the internal help.

Environment

#environment prints information about the runtime environment.

Quit

#quit ends evaluation.