Stream: Coq devs & plugin devs

Topic: Display of implicit arguments in Print vs About


view this post on Zulip Hugo Herbelin (Dec 28 2023 at 16:41):

Currently, we have e.g.:

Print id.
(*
id = fun (A : Type) (x : A) => x
     : ID

Expanded type for implicit arguments
id : forall [A : Type], A -> A

Arguments id [A] _
*)
About id.
(*
id : ID

id is not universe polymorphic
Expanded type for implicit arguments
id : forall [A : Type], A -> A

Arguments id [A] _
id is transparent
Expands to: Constant Coq.Init.Datatypes.id
*)

Otherwise said, Print displays implicit arguments after reduction but not after, while About displays them before and after reduction.

I would say that either Print should stop displaying implicit arguments at all, or it should display implicit arguments also before. Any objection at implementing one of those?

If the first case is chosen, what to do when e.g. printing an inductive type. What about replacing the current:

Print sig.
(*
Inductive sig (A : Type) (P : A -> Prop) : Type :=
    exist : forall x : A, P x -> {x : A | P x}.

Arguments sig [A]%type_scope P%type_scope
Arguments exist [A]%type_scope P%function_scope x _
*)

with

Pring sig.
(*
Inductive sig [A : Type] (P : A -> Prop) : Type :=
    exist : forall x : A, P x -> {x : A | P x}.

Arguments sig [A]%type_scope P%type_scope
Arguments exist [A]%type_scope P%function_scope x _
*)

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 17:09):

Sorry, I struggle to understand because of some typos... The last change seems a no-op? And you say "Print displays implicit arguments after reduction but not after" — I guess that "after" should read "before"?

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 17:10):

Ah, for the inductive you changed "Inductive sig" to use the appropriate parens at definition time.

view this post on Zulip Hugo Herbelin (Dec 29 2023 at 17:55):

I was not clear. Basically, I was wondering whether it would not help to show implicit arguments in Print on the type of the reference, the same as it is done for About. In particular, some users privately asked me why it was not so. See also the discussion at #14486.

view this post on Zulip Hugo Herbelin (Dec 29 2023 at 17:56):

The case of id whose type needs unfolding to reveal the implicit argument is somehow anecdotal. If I mentioned it, it is to emphasize that Print was already showing implicit arguments on such unfolded type, so that the step toward showing the implicit arguments even when no reduction is involved is not so radical. I made #18444 for that and it is open for comments. (For instance, I wonder if it is still worth to display an Arguments line once the implicit arguments are shown in the type.)

view this post on Zulip Hugo Herbelin (Dec 29 2023 at 17:56):

The case of inductive types, and thus of sig is more complex that I thought because the Inductive ... printing does not allow to show the implicit arguments of both the type and the constructors. So, in #18444, I renounced to change the situation for inductive types.

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:07):

The last problem might be a design issue with Inductive. If you write Inductive sig A ..., you don't want A to have the same status for sig and for consructors.

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:08):

I suspect Agda makes A automatically implicit for constructors.

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:11):

A definition-time option/attribute might give a backward-compatible fix, and it'd be pleasant for code that does the right thing today, via Set Implicit Arguments or via manual annotations.

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:15):

I have only thought about it quickly, you'd need to extend this to Rscord, and it definitely warrants a separate thread. But it'd mean types with parameters would have a compat printing (even if finding it seems to require backtracking)

view this post on Zulip Hugo Herbelin (Dec 30 2023 at 10:31):

Regarding inductive types, we could (in theory) evolve towards a unified syntax which makes no difference between parameters and indices and infers the role of each argument automatically (as in this CEP). In particular, we would be able to write (e.g.):

Inductive vector A n :=
| nil {A} : vector A 0
| cons {A} (a:A) {n} (l:vector A n) : vector A (S n).

where implicit arguments of constructors are indicated directly in the definition.

view this post on Zulip Paolo Giarrusso (Dec 30 2023 at 18:21):

I suspect you could write nil : vector A 0? Not sure you really need to give the user a choice


Last updated: Oct 13 2024 at 01:02 UTC