The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Are you asking: "How do I generate fresh (monomorphic?) universe variables every time I mention a particular module type in an argument list?"

Universe variables are either global, or local to a definition.  (There's a strange intermediate state when you have section-local polymorphic universes, which, if I understand correctly, are considered global while inside the section, but are replaced by definition-local universes when closing the section.)  Universe variables can't be local to modules/module types, and I don't think there's any way to get Coq to generate new universes on a Module declaration line, though I may be wrong.

The closest I could get is the following.  Is this something like what you want?

Set Universe Polymorphism.

Set Printing Universes.

Monomorphic Universe UT.

Module Type Uni.

  Monomorphic Parameter U : Type@{UT}.

  Axiom U_elim : U -> Type@{UT}.

  Coercion U_elim : U >-> Sortclass.

  Global Arguments U_elim / .

  Global Arguments U / .

End Uni.

Module U0 <: Uni.

  Monomorphic Definition U := Type.

  Definition U_elim : U -> _ := fun x => x.

End U0.

Module U1 <: Uni.

  Monomorphic Definition U := Type.

  Definition U_elim : U -> _ := fun x => x.

End U1.

Module Option (Import U : Uni) (Import U' : Uni).

  Inductive option (T : U.U) :=

  | None

  | Some (_ : T).

  Record prod (A : U.U) (B : U'.U) := pair { fst : A ; snd : B }.

End Option.

Module Option0 := Option U0 U1.

On Sat, Jan 30, 2016 at 3:58 PM, Gregory Malecha <gmalecha AT gmail.com> wrote:

Hello --

I'm wondering if there is a clean way to to make a module type that carries a universe. What I would ideally want to do is something like:

Module Type Uni.

  Universe U.

End Uni.

Module Option (U : Uni).

  Inductive option (T : Type@{U.U}) : Type :=

  | None

  | Some (_ : T).

End.

But the universe U is not accessible. My attempt, which I do not think actually works is something like this:

Module Type Uni.

  Universe U.

  Parameter type : Type@{U}.

End Uni.

Module Option (U : Uni).

  Definition U := ltac:(match type of U.type with | ?T => exact T end).

  Inductive option (t : U) : Type :=

  | None

  | Some (_ : T).

End Option.

As far as I can tell though, the universe [U] seems to be fixed, and does not vary between different instances of the module type.

Does anyone know of a way to achieve this?

Thanks.

--

gregory malecha