Generalization of Declared Variables¶
Variables to be generalized can declared with the keyword variable
.
For example:
postulate
Con : Set
variable
Γ Δ Θ : Con
Declared variables are automatically generalized in type signatures, module telescopes and data and record type parameters and indices. For example,
postulate
Sub : Con → Con → Set
id : Sub Γ Γ
-- -- equivalent to
-- id : {Γ : Con} → Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
-- -- equivalent to
-- _∘_ : {Γ Δ Θ : Con} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
Note that each type signature has a separate copy of its declared variables,
so id
and _∘_
refer to two different Γ
named variables.
When generalizing data type parameters and indicies a variable is turned into an index if it’s only mentioned in indices and into a parameter otherwise. For instance,
variable
n : Nat
data Vec (A : Set) : Nat → Set where
[] : Vec A 0
_∷_ : A → Vec A n → Vec A (suc n)
variable
A : Set
x : A
xs : Vec A n
-- Here `A` will be a parameter and `n` an index. That is,
-- data All {A : Set} (P : A → Set) : {n : Nat} → Vec A n → Set
data All (P : A → Set) : Vec A n → Set where
[] : All P []
_∷_ : P x → All P xs → All P (x ∷ xs)
The following rules are used to place the generalized variables:
- Generalized variables are placed in the front of the type signatures.
- Variables defined sooner are placed before variables defined later. (The dependencies between the variables are obeyed. The current implementation uses “smallest-numbered available vertex first” topological sorting to determine the exact order.)
variable
allows metavariables in the type of declared variables.
For example:
postulate
Ty : Con → Set
_▹_ : (Γ : Con) → Ty Γ → Con
variable
A : Ty _ -- note the underscore here
postulate
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
-- -- equivalent to
-- π₁ : {Γ Δ : Con}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
-- -- note that the metavariable was solved with Δ
Note that each type signature has a separate copy of such metavariables,
so the underscore in Ty _
can be solved differently for each type signature
which mentions A
.
Unsolved metavariables originated from variable
are generalized.
For example:
variable
σ δ ν : Sub _ _ -- metavariables: σ.1, σ.2, δ.1, δ.2, ν.1, ν.2
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
-- -- equivalent to
-- ass : {σ.1 σ.2 δ.1 ν.1 : Con}
-- {σ : Sub σ.1 σ.2}{δ : Sub δ.1 σ.1}{ν : Sub ν.1 δ.1}
-- → (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
Note that δ.2
was solved with σ.1
and ν.2
was solved with δ.1
.
If two generalizable metavariables can be solved with each-other then
the metavariable defined later will be eliminated.
Hierarchical names like δ.2
are used so one can track the origin of
the metavariables.
Currently it is not allowed to use hierarchical names when giving parameters
to functions, see Issue #3280 <https://github.com/agda/agda/issues/3280>.
Name hints of parameters are used for naming generalizable metavariables too:
postulate
Sub' : (Γ Δ : Con) → Set -- name hints for parameters of Sub'
variable
θ : Sub' _ _ -- metavariables: θ.Γ, θ.Δ
If a generalizable metavariable M is solved with term T then M is not generalized, but metavariables in T became candidates for generalization.
It is allowed to nest declared variables. For example:
variable
ℓ : Level -- let ℓ denote a level
S : Set ℓ -- let A denote a set at a level ℓ
postulate
f : S → Set ℓ
-- -- equivalent to
-- f : {ℓ ℓ' : Level}{S : Set ℓ'} → S → Set ℓ
Issues related to this feature are marked with generalize in the issue tracker: https://github.com/agda/agda/labels/generalize