Zulip Chat Archive

Stream: general

Topic: Loogle choosing tighter responses


Bolton Bailey (Oct 19 2023 at 11:54):

I am looking for an init! function with the same type as List.tail!. When I loogle for List ?_ → List ?_ I get 345 responses, and List.tail! is middle of the pack. The top responses are all functions which have multiple explicit arguments. But if I search List a -> List a on hoogle, tail and init are in the top 3 responses. @Joachim Breitner can anything be done to make loogle more like this - favoring responses which are closer to my type when explicit arguments are ignored?

Joachim Breitner (Oct 19 2023 at 12:03):

One thing that could help a lot is if you can have a _ or ?a with the additional constraint that it must be a variable in the lemma, this could already rule out any lemma where there is a List Nat or so. In theory it should actually work to write \forall a, List a -> List a, but I think in practice somehow it doesn't (debugging help welcome)

Joachim Breitner (Oct 19 2023 at 12:06):

As for sorting the results, maybe it should simply sort by lemma type size (maybe secondary after module), or number of district names (concepts) mentioned. This would automatically move stuff up that has less “extra” fluff. But then sometimes the alphabetical sorting is better at grouping related things. I doubt there is a perfect one-size-fits-all solution.

Joachim Breitner (Oct 19 2023 at 12:24):

Oh, it seems that ∀ a, List a → List a actually kinda works these days, maybe I fixed it. It matches 158 lemmas, while List ?a → List ?a matches 223 lemmas.

Joachim Breitner (Oct 19 2023 at 12:39):

Trying to sort by lemma size, I was trying to use sizeOf constInfo.type, but it seems the sizeOf instances are not computable, and I can’t find another definition for size-of-an-expr, or is there one?
(Not so important, it’s quick to write one.)

Joachim Breitner (Oct 19 2023 at 13:07):

Ok, after the next deploy it should sort lemmas (within a module) by theorem size; let’s play around with it for a while.

Joachim Breitner (Oct 19 2023 at 15:23):

It’s live now. If you search for ∀ a, List a → List a it now lists List.tail! as the first lemma of those in Init.Data.List.BasicAux, but of course plenty of lemmas from more basic modules come first. Let’s run with this for a while.

Bolton Bailey (Oct 20 2023 at 06:12):

More importantly dropLast, which is the lemma I was actually looking for, is in the top 5! Thanks!

Joachim Breitner (Oct 20 2023 at 06:55):

Great to hear! (Can't do emoji reactions on Zulip on Firefox on Android, hence posting these not very useful messages).


Last updated: Dec 20 2023 at 11:08 UTC