I'm playing around with typeclasses, and I'm running into some strange behavior: I have a Class Foo (A : Type)
which includes a function foo : A -> B
and some associated laws. When I Check foo
, I get foo : ?A -> B
, as expected. I then define a #[refine] Instance Foo Bar : Bar_Foo
and finish the proof. Now, however, Check foo
gives foo : Bar -> B
, as if it's been permanently specialized! This seems really weird to me, so I'm wondering if I'm misunderstanding something and/or how to resolve the issue.
(Another note: Set Implicit Arguments
made my typeclass stuff go absolutely haywire—removing it fixed things, but is this expected?)
Joshua Grosso said:
I'm playing around with typeclasses, and I'm running into some strange behavior: I have a
Class Foo (A : Type)
which includes a functionfoo : A -> B
and some associated laws. When ICheck foo
, I getfoo : ?A -> B
, as expected. I then define a#[refine] Instance Foo Bar : Bar_Foo
and finish the proof. Now, however,Check foo
givesfoo : Bar -> B
, as if it's been permanently specialized! This seems really weird to me, so I'm wondering if I'm misunderstanding something and/or how to resolve the issue.
Ah, if I wrap the Instance
declaration within its own section, the problem goes away—so I assume this is some sort of section-typeclass-interaction.
Further update: Adding the global
attribute to the Instance
declaration makes the specialization persist across sections.
Okay! In case anyone finds this discussion in the future: I was finally able to find a precise name for what I'm running into: "Defaulting" (according to https://github.com/DeepSpec/dsss17/blob/master/qc/Typeclasses.v#L1152, which contains more exposition). Sure enough, enabling Set Typeclasses Debug
before Check foo
shows that Bar_Foo
was the first possible instance found and therefore the one that would be used.
I guess I just hadn't expected that Check
would try to fill in a typeclass constraint :-P
To me, the most obvious solution at this point is to explicitly provide foo
all the variables in question (i.e. @foo <bla> <bla> <bla>
), but I'd much appreciate any feedback as to whether this is idiomatic or not. (Again, coming from Haskell, this all feels familiar and yet strangely weird, so I wouldn't be surprised if I'm missing something important.)
When you do a Check
it also does a typeclass search. In this case it has found that instance and filled it in. If you Print
the term you will see it has nothing to do with the instance.
I don't understand, you define an instance but you don't want it to be used?
@Gaëtan Gilbert I think what @Joshua Grosso sees is that Coq Typeclasses have the wrong mode by default
@Joshua Grosso this is not defaulting. You want #[global] Hint Mode Foo ! : typeclass_instances.
or #[global] Hint Mode Foo + : typeclass_instances.
; even better, you need to read about https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Mode.
to understand what happens to Check foo
, you'll need to use About foo.
and learn about https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments.
But I don't mean this as a hazing ritual, and I'm sorry I don't know how to phrase it better — it's just "if you're coming from Haskell, Coq typeclasses won't make sense until you learn about these N things". But let me give a summary.
(1) foo
takes a "maximally inserted" argument, so Coq tries to eagerly resolve its TC argument by searching for Foo ?A
(2) in your case there's only one instance in scope, so that's used, and ?A
is filled as an "output" of the TC search. If you add a new instance, _that_ will be used — by default, if multiple instances with the same priority apply, the last defined one is preferred.
(3) Hint Mode
can set some arguments as _inputs_ of proof search, and prevent solving Foo ?A
(4) Generally, Coq TC search is pretty different from Haskell, since it doesn't have any form of coherence
(5) What you see with Section is that Instance
is local to a section by default. This makes Instance
hard to read (are you in a section or not), so I prefer to always write #[global] Instance
or #[local] Instance
explicitly.
(1bis) to clarify: Check
does nothing special, it just takes a term; it's writing foo
in a term that triggers the search.
I guess it's time for an n-th typeclass flag telling what is the default hint mode... Should be interesting to see how much the stdlib relies on "defaulting"
I wonder if we should migrate the default like for Hint Resolve
... a difference is that modes must be declared separately (which I find a bit annoying but might be inevitable), but maybe you could ask for an attribute and warn for TCs without it.
on the stdlib, I think any TC without Hint Mode
is suspect?
I would not be a fan of introducing a modifier syntax in the term syntax. I guess an attribute is not enough in general, because we already know some people want to have two dbs with the same hint having different modes (e.g. "+ -" and "- +" to invert a bijective predicate). But for Class
maybe that would be good enough.
In logic programming languages, AFAIK, mode/world declarations are separate from the predicate declarations
@Paolo Giarrusso Not gonna lie, I was hoping it would be easier than “read the manual”... but I did have a sneaking suspicion it wouldn’t :-P
Thanks for writing up that overview; I appreciate the guidance on what exactly to learn about.
I’m wondering, could we maybe copy-and-paste your comment onto the wiki somewhere, as a sort of “Haskell to Coq typeclass migration” guide? (I just imagine I’m not the first person to run into this impedance mismatch, and probably won’t be the last.)
Paolo Giarrusso said:
I wonder if we should migrate the default like for
Hint Resolve
... a difference is that modes must be declared separately (which I find a bit annoying but might be inevitable), but maybe you could ask for an attribute and warn for TCs without it.
Maybe a mixed variant would be good: we introduce a Default Mode option, set it to "-" in compat, set it to "+" in the stdlib, and add the attribute for easier porting of the existing libraries.
That way newcommers don't have to know about the modes from the get go.
and they get the safest choice by default.
I don't think we want "!" as the default, but that it is a cheaper test to perform
@Joshua Grosso s/read the manual/understand the concepts described in those links/. Feel free to reuse my summary/paste somewhere, I'll happily license it as needed .
@Paolo Giarrusso "s/read the manual/understand the concepts described in those links/" of course, poor phrasing on my part :-)
@Matthieu Sozeau Maybe; the danger is that it'd end up like Loose Hint Behavior
:-|
@Joshua Grosso no no, poor phrasing on my part :-)
What do you mean?
If we make it "+" by default, user would need to proactively declare "less-safe" modes
Good point, there's still a way to migrate incrementally
@Matthieu Sozeau @Paolo Giarrusso https://github.com/coq/coq/issues/13083 Just found this existing discussion while researching Hint Mode
; seems like it might be related to what y'all are currently talking about
@Joshua Grosso yep — I've learned to use TCs from Ralf and Robbert's code :-)
Last updated: Oct 13 2024 at 01:02 UTC