The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I've been playing with the new universe polymorphism code in 8.5 and it is great, but I'm wondering if there is any way to declare a universe in a section and have them "cooked" at the end?

Thanks a lot.

Here is a concrete example. Suppose that I have polymorphic lists.

Set Printing Universes.

Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} :=

| pnil

| pcons : T -> plist T -> plist T.

Arguments pnil {_}.

Arguments pcons {_} _ _.

And I'd like to write the polymorphic map function. Normally (without polymorphism) I would use sections like this since the termination checker does better with this:

Section pmap.

  Variable T : Type.

  Variable U : Type.

  Variable f : T -> U.

  Polymorphic Fixpoint pmap (ls : plist T) : plist U :=

    match ls with

    | pnil => pnil

    | pcons l ls => pcons (f l) (pmap ls)

    end.

End pmap.

However, this gives me a quite strange definition.

About pmap.

(*

pmap@{Top.9 Top.13} :

forall (T : Type@{Top.7}) (U : Type@{Top.8}),

(T -> U) -> plist@{Top.9} T -> plist@{Top.13} U

(* Top.9 Top.13 |= Set <= Top.9

                   Set <= Top.13

                   Top.7 <= Top.9

                   Top.8 <= Top.13

                    *)

*)

What I'd like to get is something like this:

Polymorphic Definition pmap'@{i j} {T : Type@{i}} {U : Type@{j}} (f : T -> U)

  : plist@{i} T -> plist@{j} U :=

  fix pmap ls :=

    match ls with

    | pnil => pnil

    | pcons l ls => pcons (f l) (pmap ls)

    end.

Which has exactly the definition that I want.

About pmap'.

(*

pmap'@{i j} :

forall (T : Type@{i}) (U : Type@{j}), (T -> U) -> plist@{i} T -> plist@{j} U

(* i j |= Set <= i

          Set <= j

           *)

pmap' is universe polymorphic

Arguments T, U are implicit and maximally inserted

Argument scopes are [type_scope type_scope _ _]

pmap' is transparent

Expands to: Constant Top.pmap'

*)

Unfortunately, it can be quite annoying to write a bunch of functions out like this explicitly. The problem seems to come from the inability to name the universes in the types of T and U and continue using them later in the section.

--

gregory malecha