Functions

Functions in Arend are functions in the mathematical sense. They can have arbitrary arity. In particular, constants in Arend are just functions of arity 0. A definition of a function f consists of the signature of f followed by the body of f. The full syntax of function signatures is as follows:

\func f p_1 ... p_n : T

where f is the name of the function, p_1, … p_n are named parameters and T is the result type. In some cases specification : T of the result type can be omitted depending on the definition of function body.

There are several ways to define the body of a function. These ways are described below.

Non-recursive definitions

A non-recursive function can be defined simply by specifying an expression for the result of the function:

\func f p_1 ... p_n : T => e

where e is an expression, which must be of type T if it is specified. In such definitions the result type : T can often be omitted as the typechecker can usually infer it from e.

For example, to define the identity function on type A, write the following code:

\func id (x : A) => x

A function with three parameters that returns the second one can be defined as follows:

\func second (x : A) (y : B) (z : C) => y

You can explicitly specify the result types of these functions. The definitions above are equivalent to the following definitions:

\func id (x : A) : A => x
\func second (x : A) (y : B) (z : C) : B => y

Parameters of a function may appear in its body and in its result type.

Pattern matching

Functions can be defined by pattern matching. Let D be an inductive type with constructors con1 and con2 Nat. You can define a function which maps D to natural numbers in such a way that con1 is mapped to 0 and con2 n is mapped to suc n:

\func f (d : D) : Nat
  | con1 => 0
  | con2 n => suc n

The result type of a function defined by pattern matching must be specified explicitly. The general form of function definition by pattern matching is

\func f (x_1 : T_1) ... (x_n : T_n) : R
  | clause_1
  ...
  | clause_k

where each clause_i is of the form

p^i_1, ... p^i_n => e_i

where p^i_j is a pattern of type T_i (see below for the definition of a pattern) and e_i is an expression of type R[p^i_1/x_1, … p^i_n/x_n] (see Expressions for the discussion of the substitution operation and types of expressions). Variables x_1, … x_n are not visible in expressions e_i. Note that this construction requires all the variables to be matched on, that is the number of patterns in each clause must be n (but see below for partial pattern matching).

The clauses clause_1, … clause_k must cover all the cases. That is, if there is a pattern of the form con p_1 … p_n, where con is a constructor of a data type D, then there must be patterns of the form con’ p_1’ … p_k’ for all constructors con’ of D.

Pattern matching on constructors left and right of the interval type I is not allowed. For example, the definition \func f (i : I) : Nat | left => 0 | right => 1 is not valid.

If some of the parameters of f are implicit, corresponding patterns must be either omitted or specified explicitly by surrounding them in { }.

The definition above can be equivalently written using the keyword \with:

\func f p_1 ... p_n : R \with { | clause_1 ... | clause_k }

A pattern of type T can have one of the following forms:

  • A variable. If a variable x appears as a subpattern of p_i in a clause | p_1 … p_i … => e, it can be used in e and it will have type T. If this variable is not used anywhere, its name can be replaced with _.
  • con s_1 … s_m, where con (y_1 : A_1) … (y_m : A_m) is a constructor of a data type D and s_1 … s_m are patterns. In this case, T must be equal to D and pattern s_i must have type A_i[s_1/y_1, … s_{i-1}/y_{i-1}]. If some of the parameters of con are implicit, corresponding patterns must either be omitted or enclosed in { }.
  • (s_1, … s_m), where s_1 … s_m are patterns. In this case, T must be either a Sigma type with parameters (y_1 : A_1) … (y_m : A_m) or a class (or a record) with fields y_1 : A_1, … y_m : A_m. The pattern s_i must have type A_i[s_1/y_1, … s_{i-1}/y_{i-1}]. If m equals to 0, then T may also be a data type without constructors. In this case, the right hand side => e_i of the clause in which such a pattern appears must be omitted.

Also, a constructor or a tuple pattern may be an as-pattern. This means that there might be an expressions of the form \as x : E after the pattern, where x is a variable and E is its type which can be omitted. Then x is equivalent to this pattern.

Now, let us discuss how expressions of the form f a_1 … a_n evaluate (see Expressions for the definition of the reduction and evaluation relations). Let E be equal to f a_1 … a_n. To reduce this expression, we first evaluate expressions a_1, … a_n and match them with the patterns in the definition of f left to right, top to bottom. If all patterns p^i_1, … p^i_n matches with a_1, … a_n for some i, then E reduces to e_i[b_1/y_1, … b_k/y_k], where y_1, … y_k are variables that appear in p^i_1, … p^i_n and b_1, … b_k are subexpressions of a_1, … a_n corresponding to these variables. If some argument cannot be matched with a pattern con s_1 … s_m because it is of the form con’ … for some constructor con’ different from con, then the evaluator skips the clause with this patterns and tries the next one. If some argument cannot be matched with a pattern because it is not a constructor, then E does not reduce. If none of the clauses match with arguments, then E also does not reduce. Variables and patterns of the form (s_1, … s_m) match with any expression.

Let us consider an example. Let B be a data type with two constructors T and F. Consider the following function:

\func g (b b' : B) : Nat
  | T, _ => 0
  | _, T => 1
  | _, _ => 2

Let x be a variable and let e be an arbitrary expression. If the first argument of g a_1 a_2 is T, then the expression reduces to 0, if it is x, then the expression does not reduce since the first pattern fails to match with x. If the first argument is F, then the evaluator tries to match the second argument:

g T e => 0
g x e -- does not reduce
g F T => 1
g F F => 2
g F x -- does not reduce

Note that patterns are matched left to right, top to bottom and not the other way around. This means that even if a funcall matches the first clause, it may not evaluate. For example, consider the following definition:

\func \infix 4 < (n m : Nat) : Bool
  | _, 0 => false
  | 0, suc _ => true
  | suc n, suc m => n < m

The funcall n < 0 does not evaluate since it matches the first argument first, but funcalls 0 < 0 and suc n < 0 both evaluate to false.

Sometimes you need to write a clause in which one of the parameters is a data type without constructors. You can write pattern () which is called in this case the absurd pattern. In this case, you must omit the right hand side of the clause. For example, to define a function from the empty data type you can write:

\data Empty

\func absurd {A : \Type} (e : Empty) : A
  | ()

You can often (but not always) omit the clause with an abusrd pattern completely. For example, you can define function absurd as follows:

\func absurd {A : \Type} (e : Empty) : A

Finally, the type con1 = con2 is considered empty if con1 and con2 are disjoint constructors of some data type.

If the constructor is infix, then it can be used in the infix form in a pattern. For example, functions tail and tail’ below are equivalent:

\data List (A : \Type) | nil | \infixr 5 :: A (List A)

\func tail {A : \Type} (l : List A) : List A
  | nil => nil
  | :: _ l => l

\func tail' {A : \Type} (l : List A) : List A
  | nil => nil
  | _ :: l => l

Elim

It is often true that one only needs to pattern match on a single parameter of a function (or a few parameters), but the function has much more parameters. Then we need to repeat parameters on which we do not pattern match in each clause, which is inconvenient. In this case, we can use the \elim construction:

\func f (x_1 : A_1) ... (x_n : A_n) : R \elim x_{i_1}, ... x_{i_m}
  | p^1_1, ... p^1_m => e_1
  ...
  | p^k_1, ... p^k_m => e_k

where i_1, … i_m are integers such that 1 ≤ i_1 < … < i_m ≤ n. In this case, parameters x_{i_1}, … x_{i_m} are eliminated and are not visible in expressions e_1, … e_k. Other parameters of f are still visible in these expressions. Note that it does not matter whether a parameter x_i is explicit or implicit when it is eliminated, the corresponding pattern is always explicit.

As an example, consider the following function which chooses one of its arguments depending on the value of its other argument:

\func if (b : B) (t e : X) : X \elim b
  | T => t
  | F => e

Recursive functions

Functions defined by pattern matching can be recursive. That is, if f is a function as described above, then a reference to f may occur inside expressions e_1, … e_k. Every function in Arend is a total function. Thus, not every recursive definition is allowed. In order for such a definition to be valid, the recursion must be structural. This means that in a definition of f by pattern matching the arguments to recursive calls of f must be subpatterns of the patterns for the arguments of f.

Functions can also be mutually recursive. That is, we can have several functions which refer to each other. In this case, there must be a linear order on the set of these functions f_1, … f_n such that the signature of f_i refers only to previous functions. The bodies of the functions may refer to each other as long as the whole recursive system is structural.

Copattern matching

If the result type of a function is a record or a class, then a function can also be defined by copattern matching, which has the following syntax:

\func f (x_1 : A_1) ... (x_n : A_n) : C \cowith
  | coclause_1
  ...
  | coclause_k

where a coclause is a pair consisting of a field g of C and an expression e written g => e. Such a function has the same semantics as a definition of an instance, that is it is equivalent to the following definition:

\func f (x_1 : A_1) ... (x_n : A_n) => \new C {
  | coclause_1
  ...
  | coclause_k
}

See Class extensions for the description of the involved constructions.

Patterns in coclauses

It is possible to implement a field using pattern matching:

\func f (x_1 : A_1) ... (x_n : A_n) : C \cowith
  ...
  | field (y_1 : B_1) ... (y_k : B_k) : D \with {
    | clause_1
    ...
    | clause_m
  }
  ...

Keyword \with can be replaced with \elim as usual. Currently, clauses in such an implementation cannot refer to parameters of the function.

Lemmas

A lemma is a function, the result type of which is a proposition and the body is considered to be a proof without computational content, and, thus, it does not evaluate. To define a lemma use the keyword \lemma instead of \func. If the result type of a lemma does not belong to \Prop, but is provably a proposition, you can use the keywords \level to define a lemma with this result type. The fact that lemmas do not evaluate may greatly improve performance of typechecking if their proofs are too lengthy.

An axiom is a lemma without a body. Axioms are defined with the keyword \axiom.

\sfunc

Functions defined as \sfunc do not evaluate just as lemmas, but it is possible to evaluate such functions by using keyword \eval. Let f be an ordinary function and let a_1, … a_n be arguments such that expression f a_1 … a_n evaluates to e. If f is defined as \sfunc, then this expression won’t evaluate, but expression \eval f a_1 … a_n evaluates to e. To prove that f a_1 … a_n equals to \eval f a_1 … a_n, you can use keyword \peval. Expression \peval f a_1 … a_n has type f a_1 … a_n = \eval f a_1 … a_n.

Note that it is necessary to use \sfunc in some cases.