Stream: Coq devs & plugin devs

Topic: reduced impredicative set?

Gaëtan Gilbert (Dec 09 2022 at 11:59):

I wonder if the interesting uses of impredicative set would be satisfied by having just

Inductive Forall (A:Type) (B:A -> Set) : Set :=
  mkForall : (forall x, B x) -> Forall A B.

Definition apply {A B} (f:Forall A B) (x:A) : B x :=
  match f with mkForall f => f x end.

where Forall does NOT have large elimination (but apply s well defined because B x is small)
ie impredicative set enables 2 behaviours: the product typing rule when codomain : Set, and defining inductives in Set without large elimination whose constructors may have large arguments
perhaps just the second behaviour is enough, and it has a much more local effect so less impact on implementation

Pierre-Marie Pédrot (Dec 09 2022 at 12:16):

You lose η-laws on functions with that, but I don't know if people rely on that.

Pierre-Marie Pédrot (Dec 09 2022 at 12:17):

That said I don't consider that impredicative set is a huge burden on the implementation.

Pierre-Marie Pédrot (Dec 09 2022 at 12:17):

Most probably, I suspect it just doesn't work in practice.

Karl Palmskog (Dec 09 2022 at 12:18):

isn't the gain here that one would be able to combine code with predicative set and impredicative under one roof? (no separate option)

Pierre-Marie Pédrot (Dec 09 2022 at 12:18):

We only have a handful of tests and AFAIK no CI dev relying on it.

Pierre-Marie Pédrot (Dec 09 2022 at 12:19):

@Karl Palmskog maybe I'm misunderstanding what you mean, but that's precisely what you don't want. Otherwise you lose code reuse.

Pierre-Marie Pédrot (Dec 09 2022 at 12:19):

otherwise it's very easy to add a dedicated sort ISet that stands for impredicative set (and deactivate it by default)

Karl Palmskog (Dec 09 2022 at 12:20):

OK, so this would just change semantics with -impredicative-set I guess

Pierre-Marie Pédrot (Dec 09 2022 at 12:24):

re @Gaëtan Gilbert actually you can recover η-laws by using a primitive record instead

Pierre-Marie Pédrot (Dec 09 2022 at 12:24):

(the fact we can even do this looks like a glaring inconsistency to me but YMMV)

Gaëtan Gilbert (Dec 09 2022 at 12:52):

Pierre-Marie Pédrot said:

otherwise it's very easy to add a dedicated sort ISet that stands for impredicative set (and deactivate it by default)

I don't believe that this is true

Gaëtan Gilbert (Dec 09 2022 at 12:52):

Pierre-Marie Pédrot said:

re Gaëtan Gilbert actually you can recover η-laws by using a primitive record instead

no you can't
no large elimination without the type of product rule

Pierre-Marie Pédrot (Dec 09 2022 at 13:41):

right right

Pierre-Marie Pédrot (Dec 09 2022 at 13:42):

we could implement it with type-in-type though, and provide -impredicative-set as a library

Pierre-Marie Pédrot (Dec 09 2022 at 13:42):

(i.e. it would only activate fancy typing rules for inductive types)

Last updated: Oct 13 2024 at 01:02 UTC