Quinn (Jan 24 2022 at 19:01): Quinn (Jan 24 2022 at 19:01):When I'm debugging code dependent on itree, frequently it'll run forever rather than telling me a type error. Sometimes I can finally get it right, but I have to get lucky, the machine doesn't give me any hints because it runs forever rather than fails.
Am I not being patient enough? Should I let it search longer?
What are some techniques for speeding things up?
Karl Palmskog (Jan 24 2022 at 19:04):are you getting stuck during execution of tactics or during Qed? If the former, then you have to carefully consider the tactics you use and their parameters so they don't diverge.
Karl Palmskog (Jan 24 2022 at 19:07):tactic execution and type checking (Qed) are different, e.g., if you use a plugin such as CoqHammer, then thehammer tactic has to wait for lots of automated theorem provers (and there is nothing that in principle prevents a plugin tactic from ordering the proverbial pizza)
Quinn (Jan 24 2022 at 19:11):I think it's equivalent to during QED. it's actually in the middle of writing a Definition of something that returns an itree E unit
Karl Palmskog (Jan 24 2022 at 19:15):the whole interaction trees package seems shock-full of type classes, so it may well be type class resolution that runs amok
Karl Palmskog (Jan 24 2022 at 19:16):that's still not really type checking though, but more like "type search"
Karl Palmskog (Jan 24 2022 at 19:17):see the various typeclass debug commands here and it might make more sense: https://coq.inria.fr/refman/addendum/type-classes.html#settings
Li-yao (Jan 24 2022 at 19:42):Yes this sounds like the typical type class problems. Normally you shouldn't ever have to wait for more than one second for a definition to respond but the itree library is quite brittle on that front, so ill-typed definitions diverge instead of returning an error message. One approach worth trying is to specialize the functions you need up front, in isolated definitions that don't expose type classes in their type.
Karl Palmskog (Jan 24 2022 at 19:45):@Li-yao I don't see any Hint Mode declarations for typeclasses in the itree source, that could be a contributing factor. Have you considered adding those? (stdpp has many good examples)
Li-yao (Jan 24 2022 at 19:50):I'll definitely look into it :) The current setup is indeed as rudimentary as it gets.
Karl Palmskog (Jan 24 2022 at 19:51):OK if you don't mind I will open an issue
Emilio Jesús Gallego Arias (Jan 24 2022 at 19:52):Another very common source of problems is unification not finding a solution and taking a long time to fail. This was a huge issue on math-comp projects for example
Karl Palmskog (Jan 24 2022 at 19:54):but hint modes will help with that too, right? It will prune a lot of fruitless searches
Emilio Jesús Gallego Arias (Jan 24 2022 at 19:54):@Karl Palmskog that's unrelated I think, here I'm talking about "pure" unification
Karl Palmskog (Jan 24 2022 at 19:56):but isn't that unlikely [having pure unification problems] when using a mostly typeclass-based library?
Karl Palmskog (Jan 24 2022 at 19:59):anyway, TC and unification experts are free to weigh in or nitpick on what I wrote here: https://github.com/DeepSpec/InteractionTrees/issues/230
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:01):@Karl Palmskog I think you can also observe that wihtout TCs
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:01):if you have terms that unfold
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:02):the whole point of the locking pattern in math-comp was to avoid thi
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:02):this, for example, by forbidding unif / conversion from unfolding methods such as enum etc...
Karl Palmskog (Jan 24 2022 at 20:03):my naive impression was that those problems mainly arose during complex unification triggered by canonical structures?
Karl Palmskog (Jan 24 2022 at 20:05):but in any case, using MathComp style locking is kind of the S [top] tier of library design
Karl Palmskog (Jan 24 2022 at 20:06):is there even any paper written about it?
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:11):Not sure about where, but I've seen it covered
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:12):You don't need canonicals to have this problem, it is more like imagine some conversion problem foo ~ @enum T , that is bound to fail, but both expansions can happen, if you are unlucky the expansions can trigger exponential behavior, and then, boom
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:12):What we are missing in Coq is good tools to debug this
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:12):So in the case this happens, you can like see where the problem is more easily.
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:13):Now it is possible, but requires quite advanced skills
Karl Palmskog (Jan 24 2022 at 20:18):there are apparently a few areas in Coq where you still need to "do a PhD at X" to know about it
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:20):I wish there were just a few XD
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:20):Like most of them :D
Emilio Jesús Gallego Arias (Jan 24 2022 at 20:20):Well, I didn't do a PhD at X and I know
Karl Palmskog (Jan 24 2022 at 20:20):ok, "do a postdoc at X"
Quinn (Jan 24 2022 at 20:23):So do we think it'd be ok to enforce Typeclasses eauto := 2. and assume if it needs more than 2 layers it will diverge?
Karl Palmskog (Jan 24 2022 at 20:24):I don't think depth 2 will get you very far...
Quinn (Jan 24 2022 at 20:26):4 takes just under 20 seconds to fail, 3 takes about 2 seconds
Karl Palmskog (Jan 24 2022 at 20:27):OK, so then at least we know with reasonable certainty that typeclass resolution is the culprit, let me adjust the topic name
Quinn (Jan 24 2022 at 20:28):oh yeha, seeing a ton of useful information now. so the thread has been helpful.
Quinn (Jan 24 2022 at 20:28):I'm curious if @Li-yao has any go-to Typeclasses settings declarations for working with itrees
Karl Palmskog (Jan 24 2022 at 20:29):I think the previous advice from Li-yao is probably the way to go for now:
specialize the functions you need up front, in isolated definitions that don't expose type classes in their type.
Li-yao (Jan 24 2022 at 20:33):Yes my best advice is to not use type classes :)
Quinn (Jan 24 2022 at 20:35):My goal is to modify tutorial/Asm.v to emulate a particular architecture. I don't really know how to use itrees without blindly copying the tutorials haha
Li-yao (Jan 24 2022 at 20:35):Typeclasses eauto := is meh because it can hide errors (resolutions that should diverge end up succeeding with possibly brittle solutions).
Quinn (Jan 24 2022 at 20:37):My understanding is that the default is some Typeclasses eauto := n for some high n, and I was just lowering it but not qualitatively changing the search.
Quinn (Jan 24 2022 at 21:12):I'm not sure I understanding this advice. Does it mean to get rid of Context declarations, and bind typeclasses in function signature directly? or does it mean, if a typeclass exposes a method A -> B -> C put a general A -> B -> C in the signature of each definition _and_ delete the Context declarations?
Emilio Jesús Gallego Arias (Jan 24 2022 at 21:46):Karl Palmskog said:
there are apparently a few areas in Coq where you still need to "do a PhD at X" to know about it
Now seriously this is bad so any ideas on how to improve it are much welcome
Li-yao (Jan 24 2022 at 21:59):@Quinn IIRC the main functions using typeclasses are trigger and interp. They are usually only used with the same couple of type parameters, so for example you can make something like Definition trigger_Reg : Reg ~> itree E := trigger, and so on for every relevant effect, and then only use those monomorphic functions.
Karl Palmskog (Jan 24 2022 at 22:28):I think we all want good practices/heuristics/techniques about type class resolution and unification to become more known and reach more users, get better docs, etc., but to be produced in the research community it has be novel and/or have a nice evaluation. So if anyone can think of a nice mitigation for TC resolution divergence that is somehow measurable in lots of Coq code, I'd be happy to wrap it up nicely for a conference like ASE...
Karl Palmskog (Jan 24 2022 at 22:30):but as with many issues in Coq, people typically don't even commit code to repos with TC resolution problems, so there is not a lot to go on empirically...
Quinn (Jan 25 2022 at 04:00):Ok thanks, sounds good!
Paolo Giarrusso (Jan 25 2022 at 20:46):I agree with @Karl Palmskog 's initial suggestion: nobody ever will tell you, but to a first approximation every typeclass without a mode is a bug.
Paolo Giarrusso (Jan 25 2022 at 20:50):_in addition_, typeclass search is not going to be efficient unless you (a) pay attention so that your logic program is well-moded and as “syntax-directed” as possible (b) ideally, mark your predicates as “typeclass opaque” instead of letting unification try using every instance against every goal
Karl Palmskog (Jan 25 2022 at 20:55):argh, one might say: have a "typeclass czar" in every Coq project that uses typeclasses, and make sure that person has experience equivalent to a PhD in logic programming & type theory
Karl Palmskog (Jan 25 2022 at 21:00):@Paolo Giarrusso do you agree with the following?
using type classes is, in Greg Morrisett’s term, like steering the Queen Mary: you have to get this hulking mass pointed in the right direction so that the inference mechanism resolves things the way you want it to.
Karl Palmskog (Jan 25 2022 at 21:01):(from here: https://existentialtype.wordpress.com/2011/04/16/modules-matter-most/)
Karl Palmskog (Jan 25 2022 at 21:02):maybe in Coq it's rather more like doing maintenance in a nuclear submarine?
Paolo Giarrusso (Jan 25 2022 at 21:02):no, but I’m somewhat biased
Paolo Giarrusso (Jan 25 2022 at 21:03):it took me a while to climb the stdpp/iris learning curve, but I never did that with the math-comp one :-).
Paolo Giarrusso (Jan 25 2022 at 21:03):It _is_ nice that math-comp is getting a proper high-level language in hierarchy builder, but I _am_ concerned if you need so much code generation, since it cannot possibly be transparent to the user.
Karl Palmskog (Jan 25 2022 at 21:04):just using MathComp has always been a nice experience for me, it's when one wants to generate hierarchies it gets hard. I find just using TCs hard, not least due to stuff similar to this topic
Paolo Giarrusso (Jan 25 2022 at 21:05):a typeclass czar might be necessary today, but that’s a symptom of a problem.
Paolo Giarrusso (Jan 25 2022 at 21:05):since that’s a documentation/awareness problem, let me just say _why_ you need modes.
Paolo Giarrusso (Jan 25 2022 at 21:06):say Coq must find an instance of YourTypeclass ?evar1 ?evar2. The problem is clearly underspecified, so you might hope for an error.
Paolo Giarrusso (Jan 25 2022 at 21:07):Indeed, if you mark one or both arguments to YourTypeclass as inputs (or at least, their _heads_ as inputs), an error is what you’ll get until you constrain the problem.
Paolo Giarrusso (Jan 25 2022 at 21:08):by default, Coq will just let TC search instantiate those variables… that’s reasonable for outputs, but if you treat everything as output, Coq might just pick the last declared instance and call it a day :-(.
Paolo Giarrusso (Jan 25 2022 at 21:08):Indeed, in Lean TC arguments default to being inputs.
Karl Palmskog (Jan 25 2022 at 21:09):so should we start adding manual hint modes to that effect [inputs everywhere] in the absence of dev resources?
Karl Palmskog (Jan 25 2022 at 21:11):I think one issue is that between a project like Itrees (no hint modes) and Stdpp (expert-level hint modes), the gulf is vast, and we don't seem to have consensus or awareness what to do
Paolo Giarrusso (Jan 25 2022 at 21:11):adding mores is one good thing, but you also need to design your instances accordingly, and that part can be trickier and I don’t have a summary ready…
Paolo Giarrusso (Jan 25 2022 at 21:12):however, [hopefully] this isn’t a big problem in stdpp (or presumably itrees)
Paolo Giarrusso (Jan 25 2022 at 21:12):those are using typeclasses for overloading, not full programming
Ali Caglayan (Jan 25 2022 at 21:13):Paolo Giarrusso said:
It _is_ nice that math-comp is getting a proper high-level language in hierarchy builder, but I _am_ concerned if you need so much code generation, since it cannot possibly be transparent to the user.
I think HB does a good job at keeping things transparent. I mean there is always plan B.
Karl Palmskog (Jan 25 2022 at 21:13):so in your opinion, if all you want is overloading, you don't need to spend inordinate amounts of time thinking about instance declarations?
Paolo Giarrusso (Jan 25 2022 at 21:14):see the “hopefully” :-)
Paolo Giarrusso (Jan 25 2022 at 21:16):but I think basically yes: #[global] Hint Mode YourTypeclass ! ! : typeclass_instances. (with the right number of !) is likely to be an overall improvement.
Paolo Giarrusso (Jan 25 2022 at 21:17):and you can often see which arguments should plausibly be an output…
Karl Palmskog (Jan 25 2022 at 21:19):hmm, but we are talking unbundled classes here, right? For jumbled stuff that mixes stuff in Prop and Set/Type, I often can't make any sense of inputs or outputs
Paolo Giarrusso (Jan 25 2022 at 21:19):for instance:
(** The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K A M : Type) := lookup: K → M → option A.
Global Hint Mode Lookup - - ! : typeclass_instances.
(this one seems more liberal than I’d have expected: it can deduce the key and element type from the collection, but not viceversa, probably because of some non polymorphic collections in stdpp)
Paolo Giarrusso (Jan 25 2022 at 21:21):@Karl Palmskog I’m not sure I follow, do you have an example? stdpp does use unbundled classes, indeed
Karl Palmskog (Jan 25 2022 at 21:22):I mean that you have some monstrosity of a class that takes 4+ parameters that are not just of the varietyA : Type, and then the thing doesn't live in Prop and isn't an operational typeclass, but has 5+ fields living in various sorts.
Karl Palmskog (Jan 25 2022 at 21:25):basically, I can definitely see that the inputs/outputs are "obvious" for properly defined operational typeclasses and so on, but I'm not sure that's what people are writing in the wild
Paolo Giarrusso (Jan 25 2022 at 21:25):I can't recall those, but marking arguments as input might still be a good idea...
Paolo Giarrusso (Jan 25 2022 at 21:26):I do recall cases where modes are not obvious; my old project adds its own modes to Autosubst :-)
Karl Palmskog (Jan 25 2022 at 21:27):ah, here you have the future, packages that only add/replace modes in existing projects
Paolo Giarrusso (Jan 25 2022 at 21:27):It did quite a bit more, but certain modes made more sense for my language than for other ones
Paolo Giarrusso (Jan 25 2022 at 21:29):for the operation of “substite variables for sort A in sort B”, what’s the most appropriate mode?
Karl Palmskog (Jan 25 2022 at 21:30):OK, the "jumbled typeclass" is what one might call a "module type substitute" (basically just a way to carry around a bunch of types and facts without doing fancy proof search). And for that particular pattern, probably all inputs are the way to go.
Li-yao (Jan 25 2022 at 21:33):Would you guys have any thoughts about Set Typeclasses Strict Resolution https://coq.inria.fr/distrib/current/refman/addendum/type-classes.html#coq:flag.Typeclasses-Strict-Resolution Isn't that a "input mode by default"?
Paolo Giarrusso (Jan 25 2022 at 22:13):@Li-yao I know that @Janno tried it, and it didn't work correctly.
Paolo Giarrusso (Jan 25 2022 at 22:15):I don't think we ever dug too deeply, so it might be worth trying. It also might work well enough for most uses.
Paolo Giarrusso (Jan 25 2022 at 22:16):And remember to set it before defining the typeclass in question, this flag affects definitions not uses.
Li-yao (Jan 25 2022 at 22:37):Any rule of thumb on using mode ! vs mode +?
Paolo Giarrusso (Jan 25 2022 at 22:47):Good question... Mode ! seems most common, and often is enough to disambiguate between instances.
Paolo Giarrusso (Jan 25 2022 at 22:48):I guess a key criterion is the amount of backtracking that you're going to get; a search on an evar isn't just possibly incorrect, but it can be exponentially slow
Paolo Giarrusso (Jan 25 2022 at 22:50):but isn't that unlikely [having pure unification problems] when using a mostly typeclass-based library?
Paolo Giarrusso (Jan 25 2022 at 22:53):I forget the exact conditions, but if you have Definition foo A := list A. then you define Instance fmap_foo : FMap foo., that instance will be potentially applicable to any search for FMap bar at each level of the search.
Paolo Giarrusso (Jan 25 2022 at 22:54):TC search uses typeclasses eauto and unlike eauto, hints are not matched syntactically against goals.
Paolo Giarrusso (Jan 25 2022 at 22:55):however, if TC search sees head symbols that are (a) distinct (b) considered opaque for typeclass search (e.g. because of Typeclasses Opaque), then it can filter out the instance eagerly and skip it altogether
Quinn (Jan 26 2022 at 17:11):I might have an itree-dependent code base I'm passing off to a teammember soon. I can live with "tinker with settings if you think typeclass resolution is diverging" to an extent (not ideal), but about Hint Mode what do I say that isn't "it's an oral tradition so you're required to be in the zulip"
Quinn (Jan 26 2022 at 17:25):haha, after a Section A. containing eight Context declarations of typeclass instances, then a Definition foo : .... after End A. when I run a Check foo, it takes forever, but when I run Check @foo it returns immediately (with the contents of all the Context declarations as inputs).
I'm seeing why I have to internalize some of the advice in the thread.
Paolo Giarrusso (Jan 26 2022 at 18:02):some docs for Hint Mode do exist
Paolo Giarrusso (Jan 26 2022 at 18:02):even if they're not ideal they might be enough for the explanation...
Paolo Giarrusso (Jan 26 2022 at 18:03):in your example, what I would do is look at the output of Set Typeclasses Debug with the loop, and try to add hint modes that fix that.
Paolo Giarrusso (Jan 26 2022 at 18:04):(docs at https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Mode)
Karl Palmskog (Jan 26 2022 at 18:08):you can read the docs, or you can stare very long at Global Hint Mode ... in: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/base.v
Karl Palmskog (Jan 26 2022 at 18:09):which may actually work better in some cases
Paolo Giarrusso (Jan 26 2022 at 18:59):The other trick we don't teach is how to informally "termination-check" logic programs.
For instance, without modes and with an instance foo : TC (list A) -> TC A, you'll get an infinite loop when searching for TC ?A: Coq will just keep applying foo and you'll get goals like TC ?A -> TC (list ?A) -> TC (list (list ?A)) -> ..., hence the loop.
Quinn (Jan 31 2022 at 15:37):ok cool. thanks everyone!
Quinn (Jan 31 2022 at 15:38):@Li-yao would you say there's an opportunity for someone to refactor ITree into Module and Section _instead_ of typeclasses?
Li-yao (Jan 31 2022 at 15:53):What do you have in mind? I'm not sure modules give you the same amount of flexibility here. Instead, setting some Modes should alleviate most of the nontermination issues.
Karl Palmskog (Jan 31 2022 at 15:56):there are arguably two state-of-the-art approaches to hierarchies of structures in Coq: type classes, and packed classes w/ canonical structures. While it's in principle possible to use the module system and module types for hierarchies, they are not "first class", which means more work and less reasoning support...
Quinn (Jan 31 2022 at 16:08):Ok. I read the bob harper post linked up thread and sort of got the impression in ML-like module systems you can get many of the benefits of typeclasses. Where fulfilling the spec of a signature replaces the providing of an instance.
Karl Palmskog (Jan 31 2022 at 16:09):the key thing with type classes in Coq is that they are not a separate language feature like modules/module types are
Karl Palmskog (Jan 31 2022 at 16:11):this in my mind means that Bob's argument doesn't really cover Coq type classes. The basis for type classes is (essentially) dependent records and implicit arguments, which I don't think Bob has anything against in themselves
Karl Palmskog (Jan 31 2022 at 16:13):there isn't really any problem "instantiating" a type class several times for the same parameters in Coq, unlike in Haskell, where one might have to use compile-time configuration to get the "right" instance
Karl Palmskog (Jan 31 2022 at 16:16):this is the relevant Coq type class paper: https://hal.inria.fr/inria-00628864
Paolo Giarrusso (Feb 01 2022 at 00:10):@Karl Palmskog Harper is strongly opposed to first-class modules as well. But even if Harper is an excellent mathematicians, I’m not sure Harper wants to summarize the consensus of the community
Paolo Giarrusso (Feb 01 2022 at 00:12):but I have no idea how Harper’s view would apply to modules for dependent types. His argument against first-class modules is really for the importance of the phase distinction, but I’m not sure that’d apply to dependent types…
Enrico Tassi (Feb 01 2022 at 09:08):Quinn said:
Ok. I read the bob harper post linked up thread and sort of got the impression in ML-like module systems you can get many of the benefits of typeclasses. Where fulfilling the spec of a signature replaces the providing of an instance.
Modules are pretty much alike base instances (facts in logic programming) while functors are pretty much parametric instances (rules with premises in LP). But then type classes compose these instances automatically (using some sort of logic programming engine). I'd say that "automatic resolution of instances" is the key ingredient of "type classes".
Last updated: Apr 19 2024 at 02:02 UTC