Close to working tabled type class

[cmester0]

I have tried to implement tabled type classes to solve possible exponential time type class resolution exemplified by the diamond problem.

Any feedback or input is very welcome.

[gares]

Wow, thanks for your contribution!
I see you wrote the tabling-based search in Elpi, I hope all went well, the tooling around Elpi is very perfectible.

I'm busy right now, I can't provide a lot of feedback. I think you could complete your message with your conclusions on the experiment, like does it work, how fast, etc.

As I might have told @spitters in a private communication, with @FissoreD we have been considering implementing that algorithm in OCaml as part as Elpi itself (a bit like other Prolog engines do). I have prototype here, not integrated with Elpi but that has the same difficulties (similar data structures). Its integration with Elpi proper is in this PR LPCIC/elpi#118 but we had no time to push it.

I think your approach is interesting, especially to apply the algorithm now to existing real problems and gather feedback. I have the impression that your goals are all closed terms (no evars in there) which simplifies your indexing. Still it seems something is off with it, the comparison you provide does not seem "correct" (gt case). I think there is a correct one as a builtin, but of course it does not take Rocq's conversion rule into account, while it seems you want to.

I'll look into your code later this summer. Maybe we will meet, I plan to be at Aarhus at the time of Concur.

[spitters]

@cmester0 How long does Test1000 take with the regular {Elpi,Rocq} type class implementations?

[spitters]

Thanks @gares . Yes, let's meet in two weeks!

[cmester0]

@cmester0 How long does Test1000 take with the regular {Elpi,Rocq} type class implementations?

This is with the standard Rocq typechecker. I have not tried Elpi's typechecker yet. I am still missing some support for variables to get the Tabled Typeclass solver to work for the diamond example. I have it working for a simple term definition with only constants and variables, however, I am not entirely sure how to introduce variables (evars or free variables?) in Rocq, as Elpi terms will just collapse at the first unification test.

[cmester0]

Wow, thanks for your contribution! I see you wrote the tabling-based search in Elpi, I hope all went well, the tooling around Elpi is very perfectible.

I'm busy right now, I can't provide a lot of feedback. I think you could complete your message with your conclusions on the experiment, like does it work, how fast, etc.

As I might have told @spitters in a private communication, with @FissoreD we have been considering implementing that algorithm in OCaml as part as Elpi itself (a bit like other Prolog engines do). I have prototype here, not integrated with Elpi but that has the same difficulties (similar data structures). Its integration with Elpi proper is in this PR LPCIC/elpi#118 but we had no time to push it.

I think your approach is interesting, especially to apply the algorithm now to existing real problems and gather feedback. I have the impression that your goals are all closed terms (no evars in there) which simplifies your indexing. Still it seems something is off with it, the comparison you provide does not seem "correct" (gt case). I think there is a correct one as a builtin, but of course it does not take Rocq's conversion rule into account, while it seems you want to.

I'll look into your code later this summer. Maybe we will meet, I plan to be at Aarhus at the time of Concur.

It would probably be more optimal to implement the tabled type class in .elpi or ml directly. This is more a proof of concept and some playing around with logical programming / elpi. The benefit seems to be that it is easier to use the existing tools of Rocq/TC. There is possibly some problems, I have had issues with implementing the term comparison and the try_resovle and try_answer functions for Rocq, but I have a version working for a simpler type definition.

[cmester0]

It should work now and I can run the tower of diamond test with all 3 TC solvers, however, it seems the tabled type class solver is very slow because of updating/inserting into maps.

There might still be some missing features and possible improvements, but this should work as a starting point or proof of concept.

[spitters]

@gares do you think that using native arrays might help here?

[gares]

Sorry I'm not at my computer.

Std.map is implemented in elpi, should be decent but not fast. IMO you should expose an OCaml index on Elpi terms (no need to convert them to Rocq). There is a discrimination tree in Elpi used for a couple of purposes. We planned to base tabling on it internally, but it can be exposed as an api to elpi programs as well.

Sorry, I can't provide pointers right now.

[cmester0]

No worries, I am thankful for any pointers. To me it seems that ELPI is copying a large amount of data, which should be persistent. I will do a bit more digging, and possibly try the discrimination tree.

[gares]

The discrimination tree is here: https://github.com/LPCIC/elpi/blob/master/src/runtime/discrimination_tree.mli
It is used by the runtime, on demand, to index clauses here https://github.com/LPCIC/elpi/blob/master/src/runtime/runtime.ml#L2826 and to retrieve them https://github.com/LPCIC/elpi/blob/master/src/runtime/runtime.ml#L3103

One needs to expose it, here the code I use for OCaml's Map (on string/int/etc) https://github.com/LPCIC/elpi/blob/master/src/builtin.ml#L1185

What I propose is to expose the dtree on elpi terms, i.e. add would have type dt -> any -> any -> dt, i.e. keys/values are just elpi terms. An example of an API on raw elpi terma is occurs performing occur check https://github.com/LPCIC/elpi/blob/master/src/builtin.ml#L888 . The discrimination tree index paths, i.e. terms are seen as lists of symbols. To implement variant-based tabling one should probably change the function to create the path, since now all unif variables are considered as the same, but as a first approximation it should work. Another detail is that storing as values terms containing binders may require some extra work, but again it can come later (I suppose your search works in the initial context, it does not load new names/rules via pi during the search).