Stream: Elpi users & devs

Topic: Elpi as a Type Classes resolution engine

Janno (Feb 18 2022 at 15:38):

Thanks for all this info! I'll try out both of these options. My concrete use is an attempt to emulate something like typeclass search in elpi. I was planning to use coq-elpi's translation of constrs to add a few facts containing constrs taken from the current Coq goal. It didn't seem right to serialize the constr to text only to have it interpreted back into a constr.

Enrico Tassi (Feb 18 2022 at 16:10):

Ah ah, this thing is on my todo list as well, maybe we should join forces. I believe you should have all you need already, so unless I missed something you are probably approaching the experiment in a way which is not the easiest.

On a side note, I did not try this yet because I believe tabling (memoization) is an important feature to have in the logic programming engine if you want to implement a user friendly TC search, but I did not finish implement it yet (see https://github.com/LPCIC/elpi/pull/118). My plan was to finish this, and then do the plumbing work needed in order to take a Coq TC instance/problem and declare/solve it in Elpi.

If you think it is a good idea, we may have a chat next week on this topic.

Enrico Tassi (Feb 18 2022 at 16:12):

I mean, you should be able to do the plumbing more or less, but some of the conclusions you may draw from the experience may be "wrong" once tabling is added to Elpi.

Cyril Cohen (Feb 18 2022 at 16:14):

AFAIU the plumbing needed to solve TC using elpi already exists: i.e. hijacking Hint Extern 0 ^^'

Enrico Tassi (Feb 18 2022 at 16:15):

FTR tabling is a memoization technique that:

• avoids loops in many cases
• avoids recomputing the same solution/failure over and over

these two are problems that affect today's TC resolution engine in Coq. The absence of ! is another one, but you already have cut in Elpi.

Enrico Tassi (Feb 18 2022 at 16:15):

What I have in mind is a command elpi_tc Instance foo which is like Instance but adds a clause to Elpi's database.

Enrico Tassi (Feb 18 2022 at 16:16):

So that you can sneak that command in, say, Iris.. and then run you elpi instance resolver where you like.

Enrico Tassi (Feb 18 2022 at 16:17):

I guess sometimes you may want to add "better clauses" than the ones you can automatically generate from a Coq instance, but well it is a start.

Enrico Tassi (Feb 18 2022 at 16:19):

About running elpi in place the usual TC resolver, I think you need a hook in Coq. I don't think hints-extern can see multiple "goals", and TC resolution starts on a bunch of these. I want to see all goals in elpi, so that backtracking is on the conjunction of them, not each of them alone

Enrico Tassi (Feb 18 2022 at 16:21):

But sure, as a first approximation Hint Extern seems ok

Janno (Feb 18 2022 at 16:39):

Tabling would be absolutely amazing.

Janno (Feb 18 2022 at 16:39):

My goal is not to exactly replicate TC search but I am not sure how much more I can say right now.

Enrico Tassi (Feb 18 2022 at 17:47):

Well, if you can say more, I may help more.

The only thing I wanted to suggest is to do everything from within Coq-Elpi via coq.elpi.accumulate "dbname" (clause _ _ (pi A\ pi B\ pi C\ my_tc_search A B :- another_pred A C, and_also C B)) and Elpi Accumulate Db dbname for "global rules" and for rules local to the proof context scan the Ctx argument of goal, build clauses like the one above, and finally use NewClauses => my_tc_search ... to load them before running my_tc_search.

Enrico Tassi (Feb 18 2022 at 17:47):

Going down to the ML API of Elpi seems unnecessary to me.

Paolo Giarrusso (Feb 18 2022 at 17:49):

Regardless of @Janno's specific goals, adding a Coq hook that lets you customize TC search could help a lot for the goals that @Arthur Charguéraud mentioned yesterday

Paolo Giarrusso (Feb 18 2022 at 17:50):

if a library can provide their own TC implementation, you could try to provide unifall with that, and then get to use TCs in math-comp :-)

Enrico Tassi (Feb 18 2022 at 17:51):

Adding the hook seems quite easy, using TC in MC a bit harder ;-)

Paolo Giarrusso (Feb 18 2022 at 17:51):

I'm hinting specifically at the slide where he suggested making more of Coq extensible outside the team

Paolo Giarrusso (Feb 18 2022 at 17:51):

at least you'd fix "TCs and CS can't play together"

Enrico Tassi (Feb 18 2022 at 17:52):

I see, but you are "preaching to the converted" ("sfondi una porta aperta") with me, Coq-Elpi is quite in that direction...

Enrico Tassi (Feb 18 2022 at 17:53):

(help with the translation is welcome)

Paolo Giarrusso (Feb 18 2022 at 17:53):

also wondering :-)

Paolo Giarrusso (Feb 18 2022 at 17:53):

[actually, addingUnifall.Instance foo : type. meaning Hint Extern ... => apply: ... would be easier, I really need to start using elpi in my copious free time]

Paolo Giarrusso (Feb 18 2022 at 17:54):

I see, I'm "preaching to the choir" :-)

Enrico Tassi (Feb 18 2022 at 17:59):

To be more precise, Cyril suggests is Hint Extern => elpi new_tc_solver, and have Elpi Tactic new_tc_solver.... I was also suggesting Elpi Command declare_instance to "compile" the type of a global term into a rule used by new_tc_solver. Dunno how clear this last idea is. I do "compile clauses" in a few POC on the Coq-Elpi website, like the one about expanding records.

Paolo Giarrusso (Feb 18 2022 at 18:04):

that'd indeed be better, Unifall.Instance is just a hack for less lofty goals :-)

Janno (Feb 22 2022 at 16:11):

Enrico Tassi said:

The only thing I wanted to suggest is to do everything from within Coq-Elpi via coq.elpi.accumulate "dbname" (clause _ _ (pi A\ pi B\ pi C\ my_tc_search A B :- another_pred A C, and_also C B)) and Elpi Accumulate Db dbname for "global rules" and for rules local to the proof context scan the Ctx argument of goal, build clauses like the one above, and finally use NewClauses => my_tc_search ... to load them before running my_tc_search.

I have a slight suspicion that coq-elpi is doing too much for what I need so I'd rather start with the bare minimum and see what I need to add. Maybe I will arrive at what you propose in the end (although I do not understand any of it yet). But at least for now I want to take baby steps. (Just like baby steps, my steps seem to take a long time.)

Enrico Tassi (Feb 22 2022 at 16:48):

IMO the quickest option is that your show me something and I try to point you in the right direction. I mean, even a toy/anonymized code.

Last updated: Oct 13 2024 at 01:02 UTC