Joshua Grosso (Apr 11 2021 at 01:01): Joshua Grosso (Apr 11 2021 at 01:01):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.
Joshua Grosso (Apr 11 2021 at 01:03):(Another note: Set Implicit Arguments made my typeclass stuff go absolutely haywire—removing it fixed things, but is this expected?)
Joshua Grosso (Apr 11 2021 at 03:34):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 -> Band some associated laws. When ICheck foo, I getfoo : ?A -> B, as expected. I then define a#[refine] Instance Foo Bar : Bar_Fooand finish the proof. Now, however,Check foogivesfoo : 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.
Joshua Grosso (Apr 11 2021 at 03:49):Further update: Adding the global attribute to the Instance declaration makes the specialization persist across sections.
Joshua Grosso (Apr 11 2021 at 03:55):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
Joshua Grosso (Apr 11 2021 at 03:58):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.)
Ali Caglayan (Apr 11 2021 at 07:23):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.
Gaëtan Gilbert (Apr 11 2021 at 07:29):I don't understand, you define an instance but you don't want it to be used?
Paolo Giarrusso (Apr 11 2021 at 11:30):@Gaëtan Gilbert I think what @Joshua Grosso sees is that Coq Typeclasses have the wrong mode by default
Paolo Giarrusso (Apr 11 2021 at 11:33):@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.
Paolo Giarrusso (Apr 11 2021 at 11:35):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.
Paolo Giarrusso (Apr 11 2021 at 11:39):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.
Paolo Giarrusso (Apr 11 2021 at 11:43):(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
Paolo Giarrusso (Apr 11 2021 at 11:44):(4) Generally, Coq TC search is pretty different from Haskell, since it doesn't have any form of coherence
Paolo Giarrusso (Apr 11 2021 at 11:46):(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.
Paolo Giarrusso (Apr 11 2021 at 11:50):(1bis) to clarify: Check does nothing special, it just takes a term; it's writing foo in a term that triggers the search.
Matthieu Sozeau (Apr 11 2021 at 12:26):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"
Paolo Giarrusso (Apr 11 2021 at 16:46):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.
Paolo Giarrusso (Apr 11 2021 at 16:58):on the stdlib, I think any TC without Hint Mode is suspect?
Matthieu Sozeau (Apr 11 2021 at 18:22):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.
Matthieu Sozeau (Apr 11 2021 at 18:25):In logic programming languages, AFAIK, mode/world declarations are separate from the predicate declarations
Joshua Grosso (Apr 11 2021 at 18:52):@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.)
Matthieu Sozeau (Apr 11 2021 at 19:09):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.
Matthieu Sozeau (Apr 11 2021 at 19:09):That way newcommers don't have to know about the modes from the get go.
Matthieu Sozeau (Apr 11 2021 at 19:09):and they get the safest choice by default.
Matthieu Sozeau (Apr 11 2021 at 19:11):I don't think we want "!" as the default, but that it is a cheaper test to perform
Paolo Giarrusso (Apr 11 2021 at 19:37):@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 .
Joshua Grosso (Apr 11 2021 at 19:37):@Paolo Giarrusso "s/read the manual/understand the concepts described in those links/" of course, poor phrasing on my part :-)
Paolo Giarrusso (Apr 11 2021 at 19:38):@Matthieu Sozeau Maybe; the danger is that it'd end up like Loose Hint Behavior :-|
Paolo Giarrusso (Apr 11 2021 at 19:38):@Joshua Grosso no no, poor phrasing on my part :-)
Matthieu Sozeau (Apr 11 2021 at 19:39):What do you mean?
Matthieu Sozeau (Apr 11 2021 at 19:39):If we make it "+" by default, user would need to proactively declare "less-safe" modes
Paolo Giarrusso (Apr 11 2021 at 19:40):Good point, there's still a way to migrate incrementally
Joshua Grosso (Apr 11 2021 at 19:51):@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
Paolo Giarrusso (Apr 11 2021 at 20:05):@Joshua Grosso yep — I've learned to use TCs from Ralf and Robbert's code :-)
Last updated: Apr 20 2024 at 14:01 UTC