u/rantingpug

This has Patrick written all over it I think

I’ve been working on a dependently typed language called Yap for a while now, and I’m at the point where I’m happy enough with the direction to show it around, even though building a compiler can apparently consume years of your life and still find new ways of being utterly broken.

The playground is here: https://try-yap-next.fly.dev

And the code is here: https://github.com/tiansivive/yap

This behemoth currently has dependent types, structural row types, dependent records on those rows, implicits, liquid-style refinements, and shift/reset. A lot of that genuinely works and it's beautifully cathartic; it also just works insofar as I've conveniently ignored all the potential complications and am blissfully living in my own happy path.

The current pipeline is roughly:

parser -> bidir elaboration + NbE + first-order unification -> Core-> IVL + custom CDCL(T) verification -> GRAM -> MIR -> JS/C/Erlang

Over the past seven months I’ve spent a lot of time on GRAM: the Graph Rewriting Abstract Machine. It’s a property-graph IR for selective compilation, with a bit of MLIR inspiration. Rather than lowering once into one fixed representation, passes enrich the graph with semantic and operational structure. So far that includes eta reduction, saturation and partial applications, closure conversion, Maranget pattern compilation, and shift/reset lowering. Target code generators can then select the enrichments they need.
That graph is probably as far as I want the compiler proper to go; MIR (Mid-level IR) is a more SSA-ish bridge after it, currently very dumb and simple and just useful for experimenting and feeding three deliberately simple code generators.

I’m currently chasing meta-variable state through modules and lowering, working toward real type erasure, making verification verdicts less cryptic, and replacing “well, the snapshot changed” with meaningful tests

The next larger problems are QTT-style usage semantics, coinduction over rows and figuring out how shift/reset should actually be typed, which includes deciding whether effects will make this language cleaner or turn it into a big bog of doom.

Six months ago, before shift/reset and the current lowering path, it was probably easier to demo. I’m much happier with the design now, though. There is still a frankly unreasonable amount left to build, but that seems to be the job.

Just wanted to share!

Edit: typo and duplicate sentences