Eli Dupree (Feb 13 2024 at 11:51): 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?
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.
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?
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)
Pierre Courtieu (Feb 13 2024 at 13:46):Yes, when you use the curly braces to declare a parameter, it declares a class locally.
Pierre Courtieu (Feb 13 2024 at 13:48):Ho wait no you can't declare typeclasses themsemves on the fly.
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.
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?
Matthieu Sozeau (Feb 14 2024 at 17:02):It might be possible using notations instead?
Eli Dupree (Feb 14 2024 at 20:41):yeah I wondered about that, but my first attempt with notations got the same warning
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
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.
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?
Eli Dupree (Feb 15 2024 at 01:27):yeah, this works:
Definition test (arg : ∀ {T}, T) : False := arg.
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: Oct 13 2024 at 01:02 UTC