Lambda MicroEgg brings alpha-aware binders to e-graphs
Philip Zucker's Lambda MicroEgg extends Max Willsey's microegg with built-in binders, higher-order Miller patterns, and capture-avoiding substitution. The e-graph handles alpha equivalence and thinning-related sharing, storing liftings in a byte stolen from the u32 Id. Performance is slower than egg on AC-10 saturation but not extremely so. The tool supports lambda-free higher-order application via a curried [] constructor, and Miller patterns enable decidable higher-order matching.
Kind of you only pay hash cons memory for variables actually in use, not for the ones in scope.