Mutual Recursion

Agda offers multiple ways to write mutually-defined data types, record types and functions.

The last two are more expressive than the first one as they allow the interleaving of declarations and definitions thus making it possible for some types to refere to the constructors of a mutually-defined datatype.

Interleaved mutual blocks

Mutual recursive functions can be written by placing them inside an interleaved mutual block. The type signature of each function must come before its defining clauses and its usage sites on the right-hand side of other functions. The clauses for different functions can be interleaved e.g. for pedagogical purposes:

  1. interleaved mutual
  2. -- Declarations:
  3. even : Nat Bool
  4. odd : Nat Bool
  5. -- zero is even, not odd
  6. even zero = true
  7. odd zero = false
  8. -- suc case: switch evenness on the predecessor
  9. even (suc n) = odd n
  10. odd (suc n) = even n

You can mix arbitrary declarations, such as modules and postulates, with mutually recursive definitions. For data types and records the following syntax is used to separate the declaration from the introduction of constructors in one or many data ... where blocks:

  1. interleaved mutual
  2. -- Declaration of a product record, a universe of codes, and a decoding function
  3. record _×_ (A B : Set) : Set
  4. data U : Set
  5. El : U Set
  6. -- We have a code for the type of natural numbers in our universe
  7. data U where `Nat : U
  8. El `Nat = Nat
  9. -- Btw we know how to pair values in a record
  10. record _×_ A B where
  11. inductive; constructor _,_
  12. field fst : A; snd : B
  13. -- And we have a code for pairs in our universe
  14. data _ where
  15. _`×_ : (A B : U) → U
  16. El (A `× B) = El A × El B
  17. -- we can now build types of nested pairs of natural numbers
  18. ty-example : U
  19. ty-example = `Nat `× ((`Nat `× `Nat) `× `Nat)
  20. -- and their values
  21. val-example : El ty-example
  22. val-example = 0 , ((1 , 2) , 3)

You can mix constructors for different data types in a data _ where block (underscore instead of name).

The interleaved mutual blocks get desugared into the Forward declaration blocks described below by:

  • leaving the signatures where they are,

  • grouping the clauses for a function together with the first of them, and

  • grouping the constructors for a datatype together with the first of them.

Forward declaration

Mutual recursive functions can be written by placing the type signatures of all mutually recursive function before their definitions. The span of the mutual block will be automatically inferred by Agda:

  1. f : A
  2. g : B[f]
  3. f = a[f, g]
  4. g = b[f, g].

You can mix arbitrary declarations, such as modules and postulates, with mutually recursive definitions. For data types and records the following syntax is used to separate the declaration from the definition:

  1. -- Declaration.
  2. data Vec (A : Set) : Nat Set -- Note the absence of where’.
  3. -- Definition.
  4. data Vec A where -- Note the absence of a type signature.
  5. [] : Vec A zero
  6. _::_ : {n : Nat} A Vec A n Vec A (suc n)
  7. -- Declaration.
  8. record Sigma (A : Set) (B : A Set) : Set
  9. -- Definition.
  10. record Sigma A B where
  11. constructor _,_
  12. field fst : A
  13. snd : B fst

The parameter lists in the second part of a data or record declaration behave like variables left-hand sides (although infix syntax is not supported). That is, they should have no type signatures, but implicit parameters can be omitted or bound by name.

Such a separation of declaration and definition is for instance needed when defining a set of codes for types and their interpretation as actual types (a so-called universe):

  1. -- Declarations.
  2. data TypeCode : Set
  3. Interpretation : TypeCode Set
  4. -- Definitions.
  5. data TypeCode where
  6. nat : TypeCode
  7. pi : (a : TypeCode) (b : Interpretation a TypeCode) TypeCode
  8. Interpretation nat = Nat
  9. Interpretation (pi a b) = (x : Interpretation a) Interpretation (b x)

Note

In contrast to Interleaved mutual blocks, in forward-declaration style we can only have one data ... where block per data type.

When making separated declarations/definitions private or abstract you should attach the private keyword to the declaration and the abstract keyword to the definition. For instance, a private, abstract function can be defined as

  1. private
  2. f : A
  3. abstract
  4. f = e

Old-style mutual blocks

Mutual recursive functions can be written by placing the type signatures of all mutually recursive function before their definitions:

  1. mutual
  2. f : A
  3. f = a[f, g]
  4. g : B[f]
  5. g = b[f, g]

Using the mutual keyword, the universe example from above is expressed as follows:

  1. mutual
  2. data TypeCode : Set where
  3. nat : TypeCode
  4. pi : (a : TypeCode) (b : Interpretation a TypeCode) TypeCode
  5. Interpretation : TypeCode Set
  6. Interpretation nat = Nat
  7. Interpretation (pi a b) = (x : Interpretation a) Interpretation (b x)

This alternative syntax desugars into the new syntax by sorting the content of the mutual block into a declaration and a definition part and placing the declarations before the definitions.

Declarations comprise:

  • Type signatures of functions, data and record declarations, unquoteDecl. (Function includes here postulate and primitive etc.)

  • Module statements, such as module aliases, import and open statements.

  • Pragmas that only need the name, but not the definition of the thing they affect (e.g. INJECTIVE).

Definitions comprise:

  • Function clauses, data constructors and record definitions, unquoteDef.

  • pattern synonym definitions.

  • Pragmas that need the definition, e.g. INLINE, ETA, etc.

  • Pragmas that are not needed for type checking, like compiler pragmas.

Module definitions with module ... where are not supported in old-style mutual blocks.