Isomorphisms are back! (short talk)

on YouTube ↗11m

" summary

A library search tool called dowsing finds functions up to type isomorphism (tuples commutative/associative, unit neutral, currying) and keeps soundness and completeness while avoiding expensive full unification by precomputing lightweight heads and other shortcut features and combining them in tries. Matching is NP‑complete and unification is costly, so the system benchmarks on real data: local Open source install with 250 packages, 31,000 functions and a 10k‑function subset with many queries returning results in under 1 ms; polymorphic queries remain the slowest cases to optimize.

AI-written summary · about

" chapters (12)

1. 0:00Intro
2. 0:13Problem
3. 1:02Our tool: Dowsing!
4. 1:56Existing approaches
5. 2:50Search by type modulo isomorphism
6. 4:03Smart indexing
7. 5:15Example of metric: The head
8. 6:31Example of shortcut: Head matching - benchmarking
9. 7:15More shortcuts and combinations
10. 8:18Final benchmark
11. 9:05Conclusion
12. 9:51Ongoing work