I'm just imagining a type system based on this. I've had ideas about a Datalog-based type system before, but it was never really practical; this could be the breakthrough that would make it practical!
- Higher-Order, Data-Parallel Structured Deduction https://arxiv.org/pdf/2211.11573.pdf
- Functional Programming with Datalog https://drops.dagstuhl.de/opus/volltexte/2022/16235/pdf/LIPI...
- A Systematic Approach to Deriving Incremental Type Checkers https://www.pl.informatik.uni-mainz.de/files/2020/10/increme...