Arend Features

Arend implements a version of homotopy type theory with an interval type, which syntax is similar to cubical type theory. This implies several nice properties of path types and allows for a simple and clean definition of higher inductive types (including recursive ones). To learn more about homotopy features implemented in Arend, see below.

Arend has a powerful class system, which supports Haskell-style instance inference. Class inheritance can be used to define various hierarchies of (algebraic) structures. For a discussion of the class system, see below.

Arend also has a simple and powerful mechanism of dealing with universe levels, see here.

Homotopy Features

Arend is based on homotopy type theory with an interval type. This means that it has a built-in contractible interval type together with two constructors left, right : I. We can use this type to define the type of n-dimensional cubes as \Sigma I … I, that is as the product of n intervals. These types are not very interesting by themselves since they are contractible, but they can be used as types of cells in the definition of a higher inductive type as discussed below.

Path Types

A path in a type A between points a, a’ : A is a function f : I -> A such that f left == a and f right == a’ (we use “==” to denote the definitional equality). The type of paths is denoted a = a’. To get a path from a function and vice verse, we can use the following functions:

path (f : I -> A) : f left = f right

@ (p : a = a') : I -> A

Function @ is usually written in infix form and pronounced “at”. Function path is actually the only constructor of the data type =. Functions path and @ are mutually inverse, that is, path f @ i == f i and path (\lam i => p @ i) == p.

This definition of path types has several nice properties. First, all the usual constructions (such as concatenation of paths, transport, and the J rule) are definable for them. Moreover, some of these constructions satisfy additional computational equalities. For example, we can define the function that applies a map to a path as follows:

\func pmap {A B : \Type} (f : A -> B) {a a' : A} (p : a = a') : f a = f a'
  => path (\lam i => f (p @ i))

This function is strictly functorial, that is we have equalities pmap id p == p and pmap (\lam x => g (f x)) p == pmap g (pmap f p).

It is also easy to prove functional extensionality:

\func funExt {A : \Type} (B : A -> \Type) (f g : \Pi (x : A) -> B x) (h : \Pi (x : A) -> f x = g x) : f = g
  => path (\lam i a => h a @ i)

This function also satisfies various definitional equalities, which means that we can pass easily between equality of functions and their pointwise equality.

Higher Inductive Types

A higher inductive type is a data type that has higher cells as its constructors. For example, the 1-dimensional sphere can be defined as the data type with one point base and one 1-dimensional constructor loop attached to this point:

\data S1
  | base
  | loop I \with {
    | left => base
    | right => base
  }

Higher constructors such as loop work like ordinary functions: loop left and loop right evaluate to base. The syntax of such constructors is the same as the syntax of functions defined by pattern matching.

We can also attach cells of even higher dimensions. For example, the 2-dimensional sphere can be defined as the data type with one point base2 and one 2-dimensional constructor loop2 attached to this point. Since the boundary of 2-dimensional cube consists of four 1-dimensional cubes, we need to specify four conditions on constructor loop2:

\data S2
  | base2
  | loop2 I I \with {
    | left, _ => base2
    | right, _ => base2
    | _, left => base2
    | _, right => base2
  }

Functions over higher inductive types can be defined by pattern matching as usual. The only difference is that it is required that they respect equations on constructors. For example, to define a function S2 -> T, we need to specify one point b : T and one function l : I -> I -> T such that l left _ == b, l right _ == b, l _ left == b, and l _ left == b:

\func f (x : S2) : T
  | base2 => b
  | loop2 i j => l i j

If this definition does not satisfy the conditions described above, an error message will be generated.

Truncated Data Types

Truncated data types can be defined as higher inductive types as usual, but there is a simpler way to do this. A data type can be defined as \truncated, which means that it will be truncated to the specified homotopy level. For example, set quotients can be defined as follows:

\truncated \data Quotient {A : \Type} (R : A -> A -> \Type) : \Set
  | in~ A
  | ~-equiv (x y : A) (R x y) (i : I) \elim i {
    | left => in~ x
    | right => in~ y
  }

Such data types can be eliminated only into types of the corresponding homotopy level.

Pattern Matching

A pattern matching on a higher inductive type can be simplified if the goal has some finite homotopy level. To define a function into an n-type, it is enough to specify its values for constructors of dimension less than or equal to n + 1. For example, if X is a set, to define a function Quotient A R -> X, it is enough to specify its value for each a : A and prove that this definition respects the equivalence relation (this proof is the value corresponding to the second constructor). This works for the definition of quotients we gave above and also for quotients defined as a higher inductive type.

If P x is a proposition, to define a function \Pi (x : Quotient A R) -> P x, it is enough to specify it for the constructor in~. This becomes even more useful when P depends on several elements of the quotient. For example, if we have 3 elements x, y, z : Quotient A R (which is defined as a higher inductive type with 3 constructors), then to prove some property about them, we need to consider only one case (since its the only 0-dimensional one) instead of nine.

Class System

Arend has records and classes. Classes are just records with additional functionality, which makes them into a haskell-style type classes.

Inheritance

Records are just Sigma types with named fields. For example, we can define the type of monoids as follows:

\record Monoid (E : \Set)
  | ide : E
  | \infixl 7 * : E -> E -> E

  | ide-left (x : E) : ide * x = x
  | ide-right (x : E) : x * ide = x
  | *-assoc (x y z : E) : (x * y) * z = x * (y * z)

Records can be inherited. If a record extends some base record, then it will have the same fields as the base one together with its own fields. For example, we can define a group as a monoid together with three additional fields:

\record Group \extends Monoid
  | inverse : E -> E
  | inverse-left (x : E) : inverse x * x = ide
  | inverse-right (x : E) : x * inverse x = ide

Extensions also can implement some of the fields of the base record. Such a record is equivalent to the Sigma type which has all not implemented fields. For example, the type of commutative monoids can be defined as follows:

\record CMonoid \extends Monoid
  | *-comm (x y : E) : x * y = y * x
  | ide-right x => *-comm x ide *> ide-left x

For commutative monoids, it is enough to prove that ide is the left identity since the fact that it is the right identity follows from the commutativity. We can prove this in the definition of commutative monoids by implementing the corresponding field.

Records also support multiple inheritance. For example, we can define the type of commutative groups simply by extending the types of groups and commutative monoids:

\record CGroup \extends Group, CMonoid

Anonymous Extensions

Parameters of records are actually their fields. So, the following two definitions of pointed sets are actually equivalent:

\record Pointed (E : \Set)
  | ide : E

\record Pointed'
  | E' : \Set
  | ide' : E'

The reason why Arend does not have record parameters is because it has anonymous extensions instead. An anonymous extension of a record R is an expression of the form R { | f_1 => e_1 … | f_n => e_n }, where f_1, … f_n are fields of R and e_1, … e_n are expressions of the corresponding types. Such an expression is the same as a records which extends R and implements specified fields, but we do not have to define this record separately. The anonymous extension described above can also be written as R e_1 … e_n. In this case, fields are implemented in the same order they were defined in the record.

Let us consider some examples:

• The type Monoid is the type of monoids.
• The type Monoid Nat is the type of monoid structures on the set Nat.
• The type Monoid Nat 1 (Nat.*) is the type of proofs that 1 and Nat.* determine the structure of a monoid on Nat.

Note that the latter two examples look as if the type of monoids was defined with 1 and 3 parameters, respectively. Thus, we do not have to worry which fields should be defined as parameters and which should be left as fields. We can use any record as if it was defined in all of these styles at the same time.

Classes

Let us say we have the definition of monoids as described above. Then we want to write expressions of the form (x * y) * ide * z, but we cannot do this. The reason is that * and ide are fields. This means that they require one additional argument, an instance of Monoid. Instances of records usually cannot be inferred automatically. For this reason, it is better to define Monoid as a class. A class is defined in the same way as a record but with the keyword \class instead of \record.

Instances of classes are inferred automatically. This inference algorithm looks for instances in two places. First, it looks for parameters of a definition in which the field call is located. If there is an appropriate parameter, then it will be used as a class instance. For example, instances in the function test below will be inferred as shown in test2.

\func test {M : Monoid} (x y z : M) => (x * y) * ide * z
\func test2 {M : Monoid} (x y z : M) => (x M.* y) M.* M.ide M.* z

If there is no appropriate local instance, the algorithm will search the set of global instances. A global instance is just a function defined using the keyword \instance instead of \func. For example, we can prove that Nat is an instance of the class Monoid and use this instance as shown below:

\instance NatMonoid : Monoid Nat
  | ide => 1
  | * => Nat.*
  | ide-left x => {?} -- the proofs are omitted
  | ide-right x => {?}
  | *-assoc x y z => {?}

\func test (x y z : Nat) => (x * y) * 1 * (z * ide)

Universe Levels

Arend has a hieararchy of universes parameterized by two natural number. The first parameter corresponds to the usual (predicative) level of the universe. The second parameter corresponds to the homotopy level of types in this universe. The universe of level (p,h) is written as \h-Type p. The universe \0-Type p can be abbreviated as \Set p. We can also write \Type p h instead of \h-Type p.

Levels cannot be added with each other, but we have the successor function \suc and the maximum function \max. There is also the largest homotopy level \oo, which corresponds to untruncated types.

The universe \h-Type p belongs to the universe \(h+1)-Type (p+1). Universes are cummulative: if A : \h-Type p, then A : \h’-Type p’ for all h’ and p’ greater than or equal to h and p, respectively.

Homotopy Levels

If a type A belongs to a universe \(h+1)-Type p, the type of paths a = {A} a’ belongs to the universe \h-Type p. This means that universes of h-types behave in the same way as the usual ones (defined as subtypes of untruncated universes), but we do not have to carry around proofs that some type belongs to some homotopy level.

The Universe of Propositions

The smallest universe is \Prop, the universe of propositions. This universe is impredicative, that is it does not have the predicative level. Thus, if A is a set of any predicative level, then a = {A} a’ belongs to \Prop. Also, if B a belongs to \Prop, then this is also true for \Pi (a : A) -> B a regardless of levels of A.

Universe Polymorphism

To define a polymorphic function (or any other kind of definition), we do not have to specify levels of types explicitly. The correct level of universes usually can be inferred automatically. For example, we can define the following function:

\func test : \Type => \Type

The inferred levels of the universe in the type of the functions are greater than the levels of the universe in the body by one.

Every definition has two implicit level parameters \lp and \lh for the predicative and homotopy levels, respectively. These levels also do not have to be specified explicitly since they also can be inferred in the same way as universe levels. Consider the following examples:

\func id {A : \Type} (a : A) => a

\class Pointed (E : \Type)
  | point : E

\func test => id Pointed

The levels of the universe of the field E are inferred to (\lp, \lh). This implies that Pointed belongs to \Type (\suc \lp) (\suc \lh). Thus, the first implicit argument of the function id in the definition test is inferred to \Type (\suc \lp) (\suc \lh). This implies that the level arguments are inferred to (\suc (\suc \lp), \suc (\suc \lh)).

Language Extensions

A language extension is a Java class which is invoked during type-checking. This can be used to implement custom operations on the abstract syntax tree which are not supported by the language. They can also be used to implement various decision procedures for proof automation.

The analogical feature is macro in Agda, elaboration reflection in Idris, and Ltac in Coq.

To do this, you’ll need Arend API (you can also download its sources).