On Trivialization

Sometimes I post about Egel, but more often than not I am confronted with people who -rightfully so- wonder what the point of it all is.

Egel, the language, is a minimal front-end to an alternative operational model that showcases that term rewriting can be achieved by repeatedly rewriting the top of a directed acyclic graph. An alternative to SECD, CACM, or graph rewriting machinery like GHC's spinless tagless G-machine. I estimate that confuses people since that kind of work on operational semantics hasn't really been done for the last twenty years and this is a trivialization effort. Whereas most of the field has moved on to studying elaborate type systems that provide ever more complex static guarantees.

The keyword here is 'trivialization' and let me share my thoughts on that. I like to compare this effort to work on the Pythagorean theorem, which started off with a proof of more than twenty pages, and through insights during the last two millennia has been reduced to a one-liner.

Trivialization is important. At every step, the Pythagorean theorem didn't change, it was still true, no noteworthy things changed; similarly, Egel doesn't really show anything new, everything can already be done with other machinery, and no real unexpected exciting things are happening. Through trivialization you only get something smaller, maybe clearer. But the importance of such an effort becomes clear when one asks oneself where we would be if we were still stuck with a proof of twenty pages.

We live in an era of informatics where baroque abstraction castles are built atop of ever more complex machinery, and at the same time, there's always a need for going back to the fundamentals to see whether something is there that is less complex one can build upon to create new -maybe better- castles.