Generalization of Declared Variables

Overview

Since version 2.6.0, Agda supports implicit generalization over variables in types. Variables to be generalized over must be declared with their types in a variable block. For example:

  1. variable
  2.   ℓ : Level
  3.   n m : Nat
  5. data Vec (A : Set ℓ) : Nat → Set ℓ where
  6.   []  : Vec A 0
  7.   _∷_ : A → Vec A n → Vec A (suc n)

Here the parameter ℓ and the n in the type of _∷_ are not bound explicitly, but since they are declared as generalizable variables, bindings for them are inserted automatically. The level ℓ is added as a parameter to the datatype and n is added as an argument to _∷_. The resulting declaration is

  1. data Vec {ℓ : Level} (A : Set ℓ) : Nat → Set ℓ where
  2.   []  : Vec A 0
  3.   _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)

See Placement of generalized bindings below for more details on where bindings are inserted.

Variables are generalized in top-level type signatures, module telescopes, and record and datatype parameter telescopes.

Issues related to this feature are marked with generalize in the issue tracker.

Nested generalization

When generalizing a variable, any generalizable variables in its type are also generalized over. For instance, you can declare A to be a type at some level ℓ as

  1. variable
  2.   A : Set ℓ

Now if A is mentioned in a type, the level ℓ will also be generalized over:

  1. -- id : {A.ℓ : Level} {A : Set ℓ} → A → A
  2. id : A → A
  3. id x = x

The nesting can be arbitrarily deep, so

  1. variable
  2.   x : A
  4. refl′ : x ≡ x
  5. refl′ = refl

expands to

  1. refl′ : {x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x : x.A} → x ≡ x

See Naming of nested variables below for how the names are chosen.

Nested variables are not necessarily generalized over. In this example, if the universe level of A is fixed there is nothing to generalize:

  1. postulate
  2.   -- pure : {A : Set} {F : Set → Set} → A → F A
  3.   pure : {F : Set → Set} → A → F A

See Generalization over unsolved metavariables for more details.

Note

Nested generalized variables are local to each variable, so if you declare

  1. variable
  2.   B : Set ℓ

then A and B can still be generalized at different levels. For instance,

  1. -- _$_ : {A.ℓ : Level} {A : Set A.ℓ} {B.ℓ : Level} {B : Set B.ℓ} → (A → B) → A → B
  2. _$_ : (A → B) → A → B
  3. f $ x = f x

Generalization over unsolved metavariables

Generalization over nested variables is implemented by creating a metavariable for each nested variable and generalize over any such meta that is still unsolved after type checking. This is what makes the pure example from the previous section work: the metavariable created for ℓ is solved to level 0 and is thus not generalized over.

A typical case where this happens is when you have dependencies between different nested variables. For instance:

  1. postulate
  2.   Con : Set
  4. variable
  5.   Γ Δ Θ : Con
  7. postulate
  8.   Sub : Con → Con → Set
  10.   idS : Sub Γ Γ
  11.   _∘_ : Sub Γ Δ → Sub Δ Θ → Sub Γ Θ
  13. variable
  14.   δ σ γ : Sub Γ Δ
  16. postulate
  17.   assoc : δ ∘ (σ ∘ γ) ≡ (δ ∘ σ) ∘ γ

In the type of assoc each substitution gets two nested variable metas for their contexts, but the type of _∘_ requires the contexts of its arguments to match up, so some of these metavariables are solved. The resulting type is

  1. assoc : {δ.Γ δ.Δ : Con} {δ : Sub δ.Γ δ.Δ} {σ.Δ : Con} {σ : Sub δ.Δ σ.Δ}
  2.         {γ.Δ : Con} {γ : Sub σ.Δ γ.Δ} → (δ ∘ (σ ∘ γ)) ≡ ((δ ∘ σ) ∘ γ)

where we can see from the names that σ.Γ was unified with δ.Δ and γ.Γ with σ.Δ. In general, when unifying two metavariables the “youngest” one is eliminated which is why δ.Δ and σ.Δ are the ones that remain in the type.

If a metavariable for a nested generalizable variable is partially solved, the left-over metas are generalized over. For instance,

  1. variable
  2.   xs : Vec A n
  4. head : Vec A (suc n) → A
  5. head (x ∷ _) = x
  7. -- lemma : {xs.n.1 : Nat} {xs : Vec Nat (suc xs.n.1)} → head xs ≡ 1 → (0 < sum xs) ≡ true
  8. lemma : head xs ≡ 1 → (0 < sum xs) ≡ true

In the type of lemma a metavariable is created for the length of xs, which the application head xs refines to suc _n, for some new metavariable _n. Since there are no further constraints on _n, it’s generalized over, creating the type given in the comment. See Naming of nested variables below for how the name xs.n.1 is chosen.

Note

Only metavariables originating from nested variables are generalized over. An exception to this is in variable blocks where all unsolved metas are turned into nested variables. This means writing

  1. variable
  2.   A : Set _

is equivalent to A : Set ℓ up to naming of the nested variable (see below).

Naming of nested variables

The general naming scheme for nested generalized variables is parentVar.nestedVar. So, in the case of the identity function id : A → A expanding to

  1. id : {A.ℓ : Level} {A : Set ℓ} → A → A

the name of the level variable is A.ℓ since the name of the nested variable is ℓ and its parent is the named variable A. For multiple levels of nesting the parent can be another nested variable as in the refl′ case above

  1. refl′ : {x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x : x.A} → x ≡ x

If a nested generalizable variable is solved with a term containing further metas, these are generalized over as explained in the lemma example above. The names of the new variables are of the form parentName.i where parentName is the name of the solved variable and i numbers the metas, starting from 1, in the order they appear in the solution.

If a variable comes from a free unsolved metavariable in a variable block (see this note), its name is chosen as follows:

  • If it is a labelled argument to a function, the label is used as the name,

  • otherwise the name is its left-to-right index (starting at 1) in the list of unnamed variables in the type.

It is then given a hierarchical name based on the named variable whose type it occurs in. For example,

  1. postulate
  2.   V : (A : Set) → Nat → Set
  3.   P : V A n → Set
  5. variable
  6.   v : V _ _
  8. postulate
  9.   thm : P v

Here there are two unnamed variables in the type of v, namely the two arguments to V. The first argument has the label A in the definition of V, so this variable gets the name v.A. The second argument has no label and thus gets the name v.2 since it is the second unnamed variable in the type of v.

If the variable comes from a partially instantiated nested variable the name of the metavariable is used unqualified.

Note

Currently it is not allowed to use hierarchical names when giving parameters to functions, see Issue #3208.

Placement of generalized bindings

The following rules are used to place generalized variables:

  • Generalized variables are placed at the front of the type signature or telescope.

  • Type signatures appearing inside other type signatures, for instance in let bindings or dependent function arguments are not generalized. Instead any generalizable variables in such types are generalized over in the parent signature.

  • Variables mentioned eariler are placed before variables mentioned later, where nested variables count as being mentioned together with their parent.

Note

This means that an implicitly quantified variable cannot depend on an explicitly quantified one. See Issue #3352 for the feature request to lift this restriction.

Indexed datatypes

When generalizing datatype parameters and indicies a variable is turned into an index if it is only mentioned in indices and into a parameter otherwise. For instance,

  1. data All (P : A → Set) : Vec A n → Set where
  2.   []  : All P []
  3.   _∷_ : P x → All P xs → All P (x ∷ xs)

Here A is generalized as a parameter and n as an index. That is, the resulting signature is

  1. data All {A : Set} (P : A → Set) : {n : Nat} → Vec A n → Set where

Instance and irrelevant variables

Generalized variables are introduced as implicit arguments by default, but this can be changed to instance arguments or irrelevant arguments by annotating the declaration of the variable:

  1. record Eq (A : Set) : Set where
  2.   field eq : A → A → Bool
  4. variable
  5.   {{EqA}} : Eq A   -- generalized as an instance argument
  6.   .ignore : A      -- generalized as an irrelevant (implicit) argument

Variables are never generalized as explicit arguments.

Importing and exporting variables

Generalizable variables are treated in the same way as other declared symbols (functions, datatypes, etc) and use the same mechanisms for importing and exporting between modules. This means that unless marked private they are exported from a module.

Interaction

When developing types interactively, generalizable variables can be used in holes if they have already been generalized, but it is not possible to introduce new generalizations interactively. For instance,

  1. works : (A → B) → Vec A n → Vec B {!n!}
  2. fails : (A → B) → Vec A {!n!} → Vec B {!n!}

In works you can give n in the hole, since a binding for n has been introduced by its occurrence in the argument vector. In fails on the other hand, there is no reference to n so neither hole can be filled interactively.

Modalities

One can give a modality when declaring a generalizable variable:

  1. variable
  2.   @0 o : Nat

In the generalization process generalizable variables get the modality that they are declared with, whereas other variables always get the default modality.