Mutual definitions

A block of constants can be defined mutually. This means that first all of their types are checked, in order, so that the types of later constants in the block may refer to earlier constants (but using only their types, not their definitions). Then their definitions are checked, again in order, so that the definitions of later constants may use the definitions of earlier ones (as well as the types of arbitrary ones). Because canonical types are just a kind of definition, the same syntax for mutual definitions encompasses mutually recursive functions, mutually inductive types, inductive-inductive types, and even inductive-recursive types and functions. Furthermore, all these kinds of mutual definitions can be encoded as single definitions using record-types (but the explicit mutual syntax is usually more congenial).

The syntax for a mutual block of definitions looks just like a sequence of ordinary def commands, except that the second and later ones use the keyword and instead of def. This is similar to the syntax of ML-like programming languages and Coq, and in contrast to Agda’s style in which declarations and definitions can be mixed arbitrarily as long as each constant is declared before it is defined. We prefer to keep the declaration of the type of each constant next to its definition, and make it clear textually which blocks of constants are defined mutually, at the price of allowing the definition of a constant to refer to others whose type is declared later textually in the same block.

An entire mutual block constitutes a single command, since it is impossible to typecheck any part of it individually. It is nevertheless usual to put a blank line in between the definitions in a mutual block, although note that this cannot be done in interactive mode since a blank line ends the command.

Like any definition, the constants in a mutual block can be defined using the synthesizing form of def that omits their type. However, this is of limited usefulness, since then they cannot be used while typechecking other constants in the block, as their types are not yet known at that point.

We now give a few examples to illustrate the possibilities of mutual definitions, along with their encodings using records.

Mutual recursion

We can define the Boolean predicates even and odd on the natural numbers:

def even : ℕ → Bool ≔ [
| zero.  ↦ true.
| suc. n ↦ odd n
]

and odd : ℕ → Bool ≔ [
| zero.  ↦ false.
| suc. n ↦ even n
]

Thus, for instance, even 4 reduces to true.

Encoded as a single definition, this looks like the following.

def even_odd : (ℕ → Bool) × (ℕ → Bool) ≔ (
  [ zero. ↦ true.  | suc. n ↦ even_odd .1 n ],
  [ zero. ↦ false. | suc. n ↦ even_odd .0 n ])

Here we have used a binary product type, but in more complicated cases when doing such encoding, it may be helpful to define a custom record-type first in which the bundled family of mutually recursive functions lives.

Mutual induction

The Type-valued predicates Even and Odd can be defined similarly:

def Even : ℕ → Type ≔ data [
| even_zero. : Even zero.
| even_suc. : (n:ℕ) → Odd n → Even (suc. n)
]

and Odd : ℕ → Type ≔ data [
| odd_suc. : (n:ℕ) → Even n → Odd (suc. n)
]

Now Even 4 doesn’t reduce to anything, but it belongs to an indexed inductive type family, and can be inhabited by the term even_suc. 3 (odd_suc. 2 (even_suc. 1 (odd_suc. 0 even_zero.))).

The fact that canonical type declarations can appear as part of case trees means that these can also be encoded as a single definition:

def Even_Odd : (ℕ → Type) × (ℕ → Type) ≔ (
  data [
  | even_zero. : Even_Odd .0 zero.
  | even_suc. : (n:ℕ) → Even_Odd .1 n → Even_Odd .0 (suc. n) ],
  data [
  | odd_suc. : (n:ℕ) → Even_Odd .0 n → Even_Odd .1 (suc. n) ])

Recall that in Narya a third possibility is a recursive definition of families of canonical types:

def Even' : ℕ → Type ≔ [
| zero. ↦ sig ()
| suc. n ↦ sig (even_suc : Odd' n)
]
and Odd' : ℕ → Type ≔ [
| zero. ↦ data []
| suc. n ↦ sig (odd_suc : Even' n)
]

In this case, Even' 4 doesn’t reduce to anything, but it is definitionally a singleton, with unique inhabitant (_ ≔ (_ ≔ (_ ≔ (_ ≔ ())))).

Inductive-inductive families

An inductive-inductive definition consists of several type families defined by mutual induction, of which the types of later ones may depend on the previous ones. For example, here is a definition of the bare bones of the syntax of type theory (contexts and types) that often appears as an example of induction-induction:

def ctx : Type ≔ data [
| empty.
| ext. (Γ : ctx) (A : ty Γ)
]

and ty (Γ : ctx) : Type ≔ data [
| base.
| pi. (A : ty Γ) (B : ty (ext. Γ A))
]

Note that the context Γ is a non-uniform parameter of the datatype ty. Here is its encoding as a single definition:

def ctx_ty : Σ Type (X ↦ (X → Type)) ≔ (
  ctx ≔ data [
  | empty.
  | ext. (Γ : ctx_ty .0) (A : ctx_ty .1 Γ) ],
  ty ≔ Γ ↦ data [
  | base.
  | pi. (A : ctx_ty .1 Γ) (B : ctx_ty .1 (ext. Γ A)) ])

Inductive-recursive definitions

An inductive-recursive definition consists of one or more type families defined by induction together with one or more functions defined by recursion, in a way that refer to each other. For instance, here is an inductive-recursive universe that contains the Booleans and is closed under function-types:

def uu : Type ≔ data [
| bool.
| pi. (A : uu) (B : el A → uu)
]

and el : uu → Type ≔ [
| bool. ↦ Bool
| pi. A B ↦ (x : el A) → el (B x)
]

Because a case tree can include canonical type declarations in some branches and ordinary (co)recursive definitions in other branches, we can also encode this as a single definition:

def uu_el : Σ Type (X ↦ (X → Type)) ≔ (
  uu ≔ data [
  | bool.
  | pi. (A : uu_el .0) (B : uu_el .1 A → uu_el .0) ],
  el ≔ [
  | bool. ↦ Bool
  | pi. A B ↦ (x : uu_el .1 A) → uu_el .1 (B x) ])

Mutually recursive let-bindings

Mutual recursive families of local bindings can also be defined by following let rec with and. For instance, as a silly example we can define even without making odd globally visible:

def even (n : ℕ) : Bool ≔
  let rec even : ℕ → Bool ≔ [ zero. ↦ true. | suc. n ↦ odd n ]
  and odd : ℕ → Bool ≔ [ zero. ↦ false. | suc. n ↦ even n]
  in
  even n

Note that although the outer global def can (like any def) refer to itself recursively, the locally-bound even shadows the global one, so that even in the final line refers to the local one.

Here be dragons

As can be seen from these examples, Narya’s facility for mutual definitions is comparable to Agda’s in flexibility and power. Also like Agda, Narya currently permits even more radical things such as nested datatypes:

def Bush (A:Type) : Type ≔ data [
| leaf.
| cons. (_ : A) (_ : Bush (Bush A))
]

and poorly understood things such as mutual families of definitions including both inductive and coinductive types and both recursive and corecursive functions. As noted elsewhere, we have not yet implemented positivity, termination, or productivity checkers, so it is easy to create inconsistencies even without these more radical features. Eventually, we intend the default to be a “safe mode” that restricts mutual definitions to combinations that are known to be consistent and have understood semantics, although this could be turned off by a flag.