Stream: Coq users

Topic: Is it possible to make arguments this implicit?


view this post on Zulip Eli Dupree (Feb 13 2024 at 11:51):

I want to make an implicit parameter that's automatically passed just because it's the correct type, like typeclasses in other languages (and maybe Coq? I'm not yet familiar with typeclasses in Coq). I've tried this, but it gets an error:

Parameter P : Type -> Type.
Parameter make_T :  {T} `{P T}, T.
Definition use_make_T {T} `{P T} : T := make_T.
Errors:
The following term contains unresolved implicit arguments:
  (λ (T : Type) (P0 : P T), make_T)
More precisely:
- ?P0: Cannot infer the implicit parameter P0 of
  make_T whose type is "P T" in environment:
T : Type
P0 : P T;

Basically, I want the P T argument of use_make_T to be implicitly passed as the P T argument of make_T, but it doesn't because nothing constrains the argument to be that particular instance of P T. Is there a way to do this?

view this post on Zulip Cyril Cohen (Feb 13 2024 at 12:06):

If P is not marked as a class, Coq cannot infer an element of P T automatically. You should pass it explicitly or make sure P is a class, as in e.g.

Parameter P : Type -> Type.
Existing Class P.
Parameter make_T :  {T} `{P T}, T.
Definition use_make_T {T} `{P T} : T := make_T.

view this post on Zulip Eli Dupree (Feb 13 2024 at 12:08):

Thanks, that's pretty much what I needed to know! However, what if the class is also taken as a function parameter? Can you mark a local variable as a class?

view this post on Zulip Eli Dupree (Feb 13 2024 at 12:46):

(My actual code has an Inductive with 3 parameters that are basically typeclasses (not instances), and one of its constructors recurses with different values for those parameters, so I can't represent any of them as a global Parameter)

view this post on Zulip Pierre Courtieu (Feb 13 2024 at 13:46):

Yes, when you use the curly braces to declare a parameter, it declares a class locally.

view this post on Zulip Pierre Courtieu (Feb 13 2024 at 13:48):

Ho wait no you can't declare typeclasses themsemves on the fly.

view this post on Zulip Eli Dupree (Feb 13 2024 at 13:49):

Yeah what I want to do is this, but with P counting as a class:

Parameter make_T :  {P} {T} `{P T}, T.
Definition use_make_T {P} {T} `{P T} : T := make_T.

view this post on Zulip Eli Dupree (Feb 14 2024 at 16:26):

Oh, another question about implicit arguments. I have a bunch of types like

(some_argument :  {V} `{PropositionConstructors V} `{VExt V}, V)

which are used frequently and are verbose, so I want to make definitions to abstract out the verbosity. But when I write

Definition Vi VExt :=  {V} `{PropositionConstructors V} `{VExt V}, V.
...
(some_argument : Vi VExt)

, Coq tells me Ignoring implicit binder declaration in unexpected position. [unexpected-implicit-declaration,syntax,default]. Is there any way to keep the implicit-argument behavior without writing the full forall type inline?

view this post on Zulip Matthieu Sozeau (Feb 14 2024 at 17:02):

It might be possible using notations instead?

view this post on Zulip Eli Dupree (Feb 14 2024 at 20:41):

yeah I wondered about that, but my first attempt with notations got the same warning

view this post on Zulip Eli Dupree (Feb 14 2024 at 20:42):

there might be a more sophisticated way to use notations for it (like wrapping the binding's whole scope under the notation), but it's not obvious

view this post on Zulip Paolo Giarrusso (Feb 15 2024 at 01:23):

You can't write a definition because there's no "type of Implicit functions" in Coq; only arguments of top-level definitions can be made implicit.

view this post on Zulip Paolo Giarrusso (Feb 15 2024 at 01:26):

And I'm very surprised that some_argument can take implicits, do you have a minimal working example?

view this post on Zulip Eli Dupree (Feb 15 2024 at 01:27):

yeah, this works:

Definition test (arg :  {T}, T) : False := arg.

view this post on Zulip Eli Dupree (Feb 17 2024 at 13:20):

ha! I found a workaround that makes my initial thing work!

Definition AsClass (P : Type -> Type) := P.
Existing Class AsClass.

Parameter make_T :  {P} {T} `{AsClass P T}, T.
Definition use_make_T {P} {T} `{AsClass P T} : T := make_T.

Last updated: Jun 23 2024 at 05:02 UTC