Stream: Coq users

Topic: Template polymorphism + section variables?


view this post on Zulip Joshua Grosso (Feb 08 2021 at 18:51):

Set Auto Template Polymorphism.

Inductive foo (X : Type) : Type :=
| bar : X -> foo X.

Definition baz : Set := foo nat.

works, but

Set Auto Template Polymorphism.

Section foo.
  Variable X : Type.

  Inductive foo : Type :=
  | bar : X -> foo.
End foo.

Definition baz : Set := foo nat.

gives a universe inconsistency error. (I've fiddled around with things, and it seems like defining X as a Section-local Variable is what introduces the error in the second example.) Is there any way around this (other than not using Section-local Variables)?

view this post on Zulip Pierre-Marie Pédrot (Feb 08 2021 at 18:52):

No, it is a voluntary limitation.

view this post on Zulip Pierre-Marie Pédrot (Feb 08 2021 at 18:53):

It was changed not so long ago to fix a soundness issue of sections + template poly

view this post on Zulip Joshua Grosso (Feb 08 2021 at 19:05):

Hmm, https://github.com/coq/coq/issues/11039 seems to me to imply that universe polymorphism is the preferred approach to template polymorphism anyway—but the docs list it as experimental, so should I avoid using e.g. Set Universe Polymorphism. in modern code?

view this post on Zulip Joshua Grosso (Feb 08 2021 at 19:06):

(or does "experimental" only mean e.g. "unergonomic" rather than "potentially inconsistent")

view this post on Zulip Théo Zimmermann (Feb 08 2021 at 20:53):

"experimental" actually means that it was added as an experimental feature a long time ago and the warning was never removed from the documentation

view this post on Zulip Théo Zimmermann (Feb 08 2021 at 20:53):

But there isn't really any proper definition of what experimental features are in the case of Coq.

view this post on Zulip Théo Zimmermann (Feb 08 2021 at 20:54):

Furthermore, every universe expert will tell you that full universe polymorphism is actually better understood than what is currently implemented and known as template polymorphism in Coq.

view this post on Zulip Matthieu Sozeau (Feb 11 2021 at 19:24):

Rather the former :) The ergonomy is ongoing work as Théo mentions. If you want polymorphism just for parameters in Type@{} (and not Prop) then I would suggest making just this inductive polymorphic (and cumulative, to get a similar effect to template polymorphism)

view this post on Zulip Joshua Grosso (Feb 11 2021 at 19:44):

@Matthieu Sozeau Thanks! Just to make sure I understand: at this point, it's probably better to add#[universes(polymorphic, cumulative)] to the datatype(s) in question rather than to Set Universe Polymorphism globally?

view this post on Zulip Matthieu Sozeau (Feb 11 2021 at 19:45):

Yes. That way you shouldn't get into the trouble of having definitions with many universe binders you certainly have no use of

view this post on Zulip Matthieu Sozeau (Feb 11 2021 at 19:45):

May I ask what kind of inductive you are declaring?

view this post on Zulip Joshua Grosso (Feb 12 2021 at 04:55):

Just a basic (in)finite sequence, inside a Section.

Section seq.
  Variable X : Type.

  Inductive seq : Type :=
  | seq_infinite : (nat -> X) -> seq
  | seq_finite : list X -> seq.

  (* ... *)
End seq.

when I tried to use it (specifically, from another module) with an argument in Set, it didn't specialize to Set as I had expected.

view this post on Zulip Joshua Grosso (Feb 12 2021 at 04:59):

also I see your point—I just ran into a non-obvious universe binder issue because I I had forgotten to enable universe polymorphism somewhere else :-P


Last updated: Jan 28 2023 at 06:30 UTC