Loogle choosing tighter responses

Stream: general

[Bolton Bailey]

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]

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]

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]

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]

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]

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]

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]

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

[Joachim Breitner]

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