ezno VS rfcs

> I'm curious if there are any practical reasons we don't see them implemented in more languages.

I believe it's because they're not exactly easy to implement and the resulting extensive type checking might also affect compiler performance.

By the way, another great example of refinement types (in JavaScript) is this one: https://kaleidawave.github.io/posts/introducing-ezno/

In compilers, there's been a recent uptick in industry research and adoption into using equivalency classes and graphs (egraphs) for doing optimization passes in a way that preserves information and solves the phase ordering problem. Egg[0] was one of the big libraries that came out of it, but can only handle term rewriting without guards, and so can't express y/x*x -> y because it's unsound when x=0, or optimization passes that are across control flow points and thus some of the eclasses are only valid in some locations. The Cranelift developers adapted it into a construction they call aegraphs[1] that handles this, and are migrating Cranelift to use these passes for all optimizations, which is (hopefully) faster and achieves more optimization opportunitie; Chris Fallin is presenting about their aegraph work at PLDI this year.

0: https://egraphs-good.github.io/

1: https://github.com/cfallin/rfcs/blob/main/accepted/cranelift...