Polymorphic Universes¶
Author: | Matthieu Sozeau |
---|
General Presentation¶
Warning
The status of Universe Polymorphism is experimental.
This section describes the universe polymorphic extension of Coq. Universe polymorphism makes it possible to write generic definitions making use of universes and reuse them at different and sometimes incompatible universe levels.
A standard example of the difference between universe polymorphic and monomorphic definitions is given by the identity function:
- Definition identity {A : Type} (a : A) := a.
- identity is defined
By default, constant declarations are monomorphic, hence the identity
function declares a global universe (say Top.1
) for its domain.
Subsequently, if we try to self-apply the identity, we will get an
error:
- Fail Definition selfid := identity (@identity).
- The command has indeed failed with message: The term "@identity" has type "forall A : Type, A -> A" while it is expected to have type "?A" (unable to find a well-typed instantiation for "?A": cannot ensure that "Type@{identity.u0+1}" is a subtype of "Type@{identity.u0}").
Indeed, the global level Top.1
would have to be strictly smaller than
itself for this self-application to type check, as the type of
(@identity)
is forall (A : Type@{Top.1}), A -> A
whose type is itself
Type@{Top.1+1}
.
A universe polymorphic identity function binds its domain universe level at the definition level instead of making it global.
- Polymorphic Definition pidentity {A : Type} (a : A) := a.
- pidentity is defined
- About pidentity.
- pidentity@{Top.2} : forall A : Type, A -> A pidentity is universe polymorphic Arguments pidentity {A}%type_scope pidentity is transparent Expands to: Constant Top.pidentity
It is then possible to reuse the constant at different levels, like so:
- Definition selfpid := pidentity (@pidentity).
- selfpid is defined
Of course, the two instances of pidentity
in this definition are
different. This can be seen when the Printing Universes
flag is on:
- Set Printing Universes.
- Print selfpid.
- selfpid = pidentity@{selfpid.u0} (@pidentity@{selfpid.u1}) : forall A : Type@{selfpid.u1}, A -> A (* {selfpid.u1 selfpid.u0} |= selfpid.u1 < selfpid.u0 *) Arguments selfpid _%type_scope
Now pidentity
is used at two different levels: at the head of the
application it is instantiated at Top.3
while in the argument position
it is instantiated at Top.4
. This definition is only valid as long as
Top.4
is strictly smaller than Top.3
, as shown by the constraints. Note
that this definition is monomorphic (not universe polymorphic), so the
two universes (in this case Top.3
and Top.4
) are actually global
levels.
When printing pidentity
, we can see the universes it binds in
the annotation @{Top.2}
. Additionally, when
Printing Universes
is on we print the "universe context" of
pidentity
consisting of the bound universes and the
constraints they must verify (for pidentity
there are no constraints).
Inductive types can also be declared universes polymorphic on universes appearing in their parameters or fields. A typical example is given by monoids:
- Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car; mon_op : mon_car -> mon_car -> mon_car }.
- Monoid is defined mon_car is defined mon_unit is defined mon_op is defined
- Print Monoid.
- Record Monoid : Type@{Top.6+1} := Build_Monoid { mon_car : Type@{Top.6}; mon_unit : mon_car; mon_op : mon_car -> mon_car -> mon_car } (* Top.6 |= *) Arguments Build_Monoid _%type_scope _ _%function_scope
The Monoid's carrier universe is polymorphic, hence it is possible to
instantiate it for example with Monoid
itself. First we build the
trivial unit monoid in Set
:
- Definition unit_monoid : Monoid := {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}.
- unit_monoid is defined
From this we can build a definition for the monoid of Set
-monoids
(where multiplication would be given by the product of monoids).
- Polymorphic Definition monoid_monoid : Monoid.
- 1 subgoal ============================ Monoid@{Top.9}
- refine (@Build_Monoid Monoid unit_monoid (fun x y => x)).
- No more subgoals.
- Defined.
- Print monoid_monoid.
- monoid_monoid@{Top.9} = {| mon_car := Monoid@{Set}; mon_unit := unit_monoid; mon_op := fun x _ : Monoid@{Set} => x |} : Monoid@{Top.9} (* Top.9 |= Set < Top.9 *)
As one can see from the constraints, this monoid is “large”, it lives
in a universe strictly higher than Set
.
Polymorphic, Monomorphic¶
-
Command
Polymorphic definition
¶ As shown in the examples, polymorphic definitions and inductives can be declared using the
Polymorphic
prefix.
-
Flag
Universe Polymorphism
¶ Once enabled, this flag will implicitly prepend
Polymorphic
to any definition of the user.
-
Command
Monomorphic definition
¶ When the
Universe Polymorphism
flag is set, to make a definition producing global universe constraints, one can use theMonomorphic
prefix.
Many other commands support the Polymorphic
flag, including:
Lemma
,Axiom
, and all the other “definition” keywords support polymorphism.Section
will locally set the polymorphism flag inside the section.Variables
,Context
,Universe
andConstraint
in a section support polymorphism. See Universe polymorphism and sections for more details.Hint Resolve
andHint Rewrite
will use the auto/rewrite hint polymorphically, not at a single instance.
Cumulative, NonCumulative¶
Polymorphic inductive types, coinductive types, variants and records can be
declared cumulative using the Cumulative
prefix.
Alternatively, there is a Polymorphic Inductive
Cumulativity
flag which when set, makes all subsequent polymorphic
inductive definitions cumulative. When set, inductive types and the
like can be enforced to be non-cumulative using the NonCumulative
prefix.
-
Flag
Polymorphic Inductive Cumulativity
¶ When this flag is on, it sets all following polymorphic inductive types as cumulative (it is off by default).
Consider the examples below.
- Polymorphic Cumulative Inductive list {A : Type} := | nil : list | cons : A -> list -> list.
- list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
- Print list.
- Inductive list@{Top.12} (A : Type@{Top.12}) : Type@{max(Set,Top.12)} := nil : list@{Top.12} | cons : A -> list@{Top.12} -> list@{Top.12} (* *Top.12 |= *) Arguments list {A}%type_scope Arguments nil {A}%type_scope Arguments cons {A}%type_scope
When printing list
, the universe context indicates the subtyping
constraints by prefixing the level names with symbols.
Because inductive subtypings are only produced by comparing inductives
to themselves with universes changed, they amount to variance
information: each universe is either invariant, covariant or
irrelevant (there are no contravariant subtypings in Coq),
respectively represented by the symbols =
, +
and *
.
Here we see that list
binds an irrelevant universe, so any two
instances of list
are convertible: \(E[Γ] ⊢ \mathsf{list}@\{i\}~A
=_{βδιζη} \mathsf{list}@\{j\}~B\) whenever \(E[Γ] ⊢ A =_{βδιζη} B\) and
this applies also to their corresponding constructors, when
they are comparable at the same type.
See Conversion rules for more details on convertibility and subtyping. The following is an example of a record with non-trivial subtyping relation:
- Polymorphic Cumulative Record packType := {pk : Type}.
- packType is defined pk is defined
packType
binds a covariant universe, i.e.
Cumulative inductive types, coinductive types, variants and records
only make sense when they are universe polymorphic. Therefore, an
error is issued whenever the user uses the Cumulative
or
NonCumulative
prefix in a monomorphic context.
Notice that this is not the case for the Polymorphic Inductive Cumulativity
flag.
That is, this flag, when set, makes all subsequent polymorphic
inductive declarations cumulative (unless, of course the NonCumulative
prefix is used)
but has no effect on monomorphic inductive declarations.
Consider the following examples.
- Fail Monomorphic Cumulative Inductive Unit := unit.
- The command has indeed failed with message: The Cumulative prefix can only be used in a polymorphic context.
- Fail Monomorphic NonCumulative Inductive Unit := unit.
- The command has indeed failed with message: The NonCumulative prefix can only be used in a polymorphic context.
- Set Polymorphic Inductive Cumulativity.
- Inductive Unit := unit.
- Unit is defined Unit_rect is defined Unit_ind is defined Unit_rec is defined Unit_sind is defined
An example of a proof using cumulativity¶
- Set Universe Polymorphism.
- Set Polymorphic Inductive Cumulativity.
- Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
- eq is defined eq_rect is defined eq_ind is defined eq_rec is defined eq_sind is defined
- Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) := forall f g : (forall a, B a), (forall x, eq@{e} (f x) (g x)) -> eq@{e} f g.
- funext_type is defined
- Section down.
- Universes a b e e'.
- Constraint e' < e.
- Lemma funext_down {A B} (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B.
- 1 subgoal A : Type B : A -> Type H : funext_type A B ============================ funext_type A B
- Proof.
- exact H.
- No more subgoals.
- Defined.
- End down.
Cumulativity Weak Constraints¶
-
Flag
Cumulativity Weak Constraints
¶ When set, which is the default, causes "weak" constraints to be produced when comparing universes in an irrelevant position. Processing weak constraints is delayed until minimization time. A weak constraint between
u
andv
when neither is smaller than the other and one is flexible causes them to be unified. Otherwise the constraint is silently discarded.This heuristic is experimental and may change in future versions. Disabling weak constraints is more predictable but may produce arbitrary numbers of universes.
Global and local universes¶
Each universe is declared in a global or local environment before it
can be used. To ensure compatibility, every global universe is set
to be strictly greater than Set
when it is introduced, while every
local (i.e. polymorphically quantified) universe is introduced as
greater or equal to Set
.
Conversion and unification¶
The semantics of conversion and unification have to be modified a little to account for the new universe instance arguments to polymorphic references. The semantics respect the fact that definitions are transparent, so indistinguishable from their bodies during conversion.
This is accomplished by changing one rule of unification, the first- order approximation rule, which applies when two applicative terms with the same head are compared. It tries to short-cut unfolding by comparing the arguments directly. In case the constant is universe polymorphic, we allow this rule to fire only when unifying the universes results in instantiating a so-called flexible universe variables (not given by the user). Similarly for conversion, if such an equation of applicative terms fail due to a universe comparison not being satisfied, the terms are unfolded. This change implies that conversion and unification can have different unfolding behaviors on the same development with universe polymorphism switched on or off.
Minimization¶
Universe polymorphism with cumulativity tends to generate many useless
inclusion constraints in general. Typically at each application of a
polymorphic constant f
, if an argument has expected type Type@{i}
and is given a term of type Type@{j}
, a \(j ≤ i\) constraint will be
generated. It is however often the case that an equation \(j = i\) would
be more appropriate, when f
's universes are fresh for example.
Consider the following example:
- Polymorphic Definition pidentity {A : Type} (a : A) := a.
- pidentity is defined
- Set Printing Universes.
- Definition id0 := @pidentity nat 0.
- id0 is defined
- Print id0.
- id0@{} = pidentity@{Set} 0 : nat
This definition is elaborated by minimizing the universe of id0
to
level Set
while the more general definition would keep the fresh level
i
generated at the application of id
and a constraint that Set
\(≤ i\).
This minimization process is applied only to fresh universe variables.
It simply adds an equation between the variable and its lower bound if
it is an atomic universe (i.e. not an algebraic max() universe).
-
Flag
Universe Minimization ToSet
¶ Turning this flag off (it is on by default) disallows minimization to the sort
Set
and only collapses floating universes between themselves.
Explicit Universes¶
The syntax has been extended to allow users to explicitly bind names to universes and explicitly instantiate polymorphic definitions.
-
Command
Universe ident
¶ -
Command
Polymorphic Universe ident
¶ In the monorphic case, this command declares a new global universe named
ident
, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The command supports thePolymorphic
flag only in sections, meaning the universe quantification will be discharged on each section definition independently.
-
Command
Constraint universe_constraint
¶ -
Command
Polymorphic Constraint universe_constraint
¶ This command declares a new constraint between named universes.
universe_constraint ::=
qualid
<qualid
qualid
<=qualid
qualid
=qualid
If consistent, the constraint is then enforced in the global environment. Like
Universe
, it can be used with thePolymorphic
prefix in sections only to declare constraints discharged at section closing time. One cannot declare a global constraint on polymorphic universes.-
Error
Universe inconsistency.
¶
-
Error
Polymorphic definitions¶
For polymorphic definitions, the declaration of (all) universe levels introduced by a definition uses the following syntax:
- Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A.
- le is defined
- Print le.
- le@{i j} = fun A : Type@{i} => A : Type@{i} -> Type@{j} (* i j |= i <= j *) Arguments le _%type_scope
During refinement we find that j
must be larger or equal than i
, as we
are using A : Type@{i} <= Type@{j}
, hence the generated constraint. At the
end of a definition or proof, we check that the only remaining
universes are the ones declared. In the term and in general in proof
mode, introduced universe names can be referred to in terms. Note that
local universe names shadow global universe names. During a proof, one
can use Show Universes
to display the current context of universes.
Definitions can also be instantiated explicitly, giving their full instance:
- Check (pidentity@{Set}).
- pidentity@{Set} : ?A -> ?A where ?A : [ |- Set]
- Monomorphic Universes k l.
- Check (le@{k l}).
- le@{k l} : Type@{k} -> Type@{l} (* {} |= k <= l *)
User-named universes and the anonymous universe implicitly attached to
an explicit Type
are considered rigid for unification and are never
minimized. Flexible anonymous universes can be produced with an
underscore or by omitting the annotation to a polymorphic definition.
- Check (fun x => x) : Type -> Type.
- (fun x : Type@{Top.51} => x) : Type@{Top.51} -> Type@{Top.52} : Type@{Top.51} -> Type@{Top.52} (* {Top.52 Top.51} |= Top.51 <= Top.52 *)
- Check (fun x => x) : Type -> Type@{_}.
- (fun x : Type@{Top.53} => x) : Type@{Top.53} -> Type@{Top.53} : Type@{Top.53} -> Type@{Top.53} (* {Top.53} |= *)
- Check le@{k _}.
- le@{k k} : Type@{k} -> Type@{k}
- Check le.
- le@{Top.56 Top.56} : Type@{Top.56} -> Type@{Top.56} (* {Top.56} |= *)
-
Flag
Strict Universe Declaration
¶ Turning this flag off allows one to freely use identifiers for universes without declaring them first, with the semantics that the first use declares it. In this mode, the universe names are not associated with the definition or proof once it has been defined. This is meant mainly for debugging purposes.
-
Flag
Private Polymorphic Universes
¶ This flag, on by default, removes universes which appear only in the body of an opaque polymorphic definition from the definition's universe arguments. As such, no value needs to be provided for these universes when instantiating the definition. Universe constraints are automatically adjusted.
Consider the following definition:
- Lemma foo@{i} : Type@{i}.
- 1 subgoal ============================ Type@{i}
- Proof.
- exact Type.
- No more subgoals.
- Qed.
- Print foo.
- foo@{i} = Type@{Top.59} : Type@{i} (* Public universes: i |= Set < i Private universes: {Top.59} |= Top.59 < i *)
The universe
Top.xxx
for theType
in the body cannot be accessed, we only care that one exists for any instantiation of the universes appearing in the type offoo
. This is guaranteed when the transitive constraintSet <= Top.xxx < i
is verified. Then when using the constant we don't need to put a value for the inner universe:- Check foo@{_}.
- foo@{Top.60} : Type@{Top.60} (* {Top.60} |= Set < Top.60 *)
and when not looking at the body we don't mention the private universe:
- About foo.
- foo@{i} : Type@{i} (* i |= Set < i *) foo is universe polymorphic foo is opaque Expands to: Constant Top.foo
To recover the same behaviour with regard to universes as
Defined
, thePrivate Polymorphic Universes
flag may be unset:- Unset Private Polymorphic Universes.
- Lemma bar : Type.
- 1 subgoal ============================ Type@{Top.61}
- Proof.
- exact Type.
- No more subgoals.
- Qed.
- About bar.
- bar@{Top.61 Top.62} : Type@{Top.61} (* Top.61 Top.62 |= Top.62 < Top.61 *) bar is universe polymorphic bar is opaque Expands to: Constant Top.bar
- Fail Check bar@{_}.
- The command has indeed failed with message: Universe instance should have length 2.
- Check bar@{_ _}.
- bar@{Top.64 Top.65} : Type@{Top.64} (* {Top.65 Top.64} |= Top.65 < Top.64 *)
Note that named universes are always public.
- Set Private Polymorphic Universes.
- Unset Strict Universe Declaration.
- Lemma baz : Type@{outer}.
- 1 subgoal ============================ Type@{outer}
- Proof.
- exact Type@{inner}.
- No more subgoals.
- Qed.
- About baz.
- baz@{outer inner} : Type@{outer} (* outer inner |= inner < outer *) baz is universe polymorphic baz is opaque Expands to: Constant Top.baz
Universe polymorphism and sections¶
Variables
, Context
, Universe
and
Constraint
in a section support polymorphism. This means that
the universe variables and their associated constraints are discharged
polymorphically over definitions that use them. In other words, two
definitions in the section sharing a common variable will both get
parameterized by the universes produced by the variable declaration.
This is in contrast to a “mononorphic” variable which introduces
global universes and constraints, making the two definitions depend on
the same global universes associated to the variable.
It is possible to mix universe polymorphism and monomorphism in sections, except in the following ways:
no monomorphic constraint may refer to a polymorphic universe:
- Section Foo.
- Polymorphic Universe i.
- Fail Constraint i = i.
- The command has indeed failed with message: Cannot add monomorphic constraints which refer to section polymorphic universes.
This includes constraints implictly declared by commands such as
Variable
, which may as a such need to be used with universe polymorphism activated (locally by attribute or globally by option):- Fail Variable A : (Type@{i} : Type).
- The command has indeed failed with message: Cannot add monomorphic constraints which refer to section polymorphic universes.
- Polymorphic Variable A : (Type@{i} : Type).
- A is declared
(in the above example the anonymous
Type
constrains polymorphic universei
to be strictly smaller.)no monomorphic constant or inductive may be declared if polymorphic universes or universe constraints are present.
These restrictions are required in order to produce a sensible result when closing the section (the requirement on constants and inductives is stricter than the one on constraints, because constants and inductives are abstracted by all the section's polymorphic universes and constraints).