Open spitters opened 5 years ago
Yep, definitely would be great to have a HoTT/full-DTT compatible congruence, whereas Coq's current congruence closure algorithm does not handle dependency at all. We're thinking with N. Tabareau and E. Tanter that the "Equivalences for Free" parametricity + univalence translation + Soccola's idea could be mixed to give that a kind of generalized congruence with equality/equivalences working with dependency.
That sounds great.
@spitters pointed me toward this thread. I've been thinking a lot about better congruence in HoTT. I think that the root of what you want is proof-producing e-graphs with equality up to transport as the notion of equality. I wrote a blog post about it here.
I link in that blog post to Leo de Moura's work in Lean, but in fact I think in HoTT it would be much simper and look not very different from what you'd do in a simply-typed logic, since HoTT gives you a much nicer notion of congruence over dependent types (seems to me that what the paper you linked to states as congruence is what Leo calls hcongr_ideal
, except with the notion of equality we actually want).
I think it's even cooler than "just" implementing better congruence in HoTT though: The same exact data structure and algorithm could get you more efficient type-based search for automatic transport for large libraries than what you get using type classes, since you can think of this automatic transport as just being a rewrite system. I suspect it would be useful for congruence, but also for type-based automatic transport in DEVOID, in the univalent parametricity framework, and in CoqHoTT.
If there's enough critical interest, I'm happy to contribute to developing them. I'm talking to a number of people here at UW who work on e-graphs because I also need something similar for DEVOID. Regardless, I'd like to be looped in to whatever happens here.
I am thrilled that this is true!
This same insight means that you should be able to use egraphs to implement efficient type-directed search for automatic transport.
@spitters, out of curiosity, what is broken about the commented out test cases in Examples.agda?
We are looking at the implementation as part of a reading group that includes me along with a lot of e-graph experts, with an eye on very efficient implementations of transport for cubical and later for HoTT. We were wondering why those cases aren't working yet.
I recall that they were just slow. @limemloh will confirm. In fact, I believe performance even improved with a later version of agda.
@tlringer Exciting. I'm looking forward to your findings.
Thanks! Some thoughts from the reading group. For reference, Zach, Max, Chandra, and Remy are e-graph experts. My background is in proof automation and proof engineering more broadly (Zach also knows a lot about proof engineering).
My current absolutely crazy plan is to implement a simple version of cubical in Rust and try to back it by egg for efficient automatic transport with type-based search. This is a side project so I don't anticipate it being serious research for now, and I'm happy to have external contributions if anyone feels like trying, but I think understanding it well in cubical before moving on to HoTT is a good idea. (It might even be enough for me---I might be able to make my tool's metatheory cubical.)
Hello Bas, glad to be chatting with you again :) To clarify, in our applications the graph contains two kinds of edges: 1. an equality edge from (the root of) a term to another term, and 2. an "AST" edge from an operator to its arguments (which are representatives of equivalent classes). E.g. from + to a and from + to b. We think the acyclic requirement applies only to equality edges. In fact it's not obvious you need AST edges here.
For future reference. This extension of the algorithm behind the congruence tactic that is compatible with HoTT.