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 _
*)
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"?
Ah, for the inductive you changed "Inductive sig" to use the appropriate parens at definition time.
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.
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.)
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.
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.
I suspect Agda makes A automatically implicit for constructors.
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.
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)
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.
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