Apologies in advance for the word geyser.
[Trying to avoid saturating my ask with my own opinions.]
[Trying to nerdsnipe myself into actually working on this project now that I have a name for it.]
Personally I've been thinking that a nice FP language with algebraic effects and various abstractions to ease the “bare logic -> full fledged implementation” transition would work quite well, be rather easy to compile, and still enable WYSIWYG. But uh … maybe I need to actually implement it to back up my claims.
What I want out of my metatheory is the wish list I compiled while trying to craft my Dhall-PureScript project. (Sorry for all who wanted that to materialize lol.)
There's two pillars:
- Things that are just painful in Haskelly languages, like pattern matching
- Pushing the philosophical boundaries of how to implement type theories
Pattern matching is painful because we want to act like there is just one expression type, but all the cruft we add on top gets in the way, especially in languages where you are bound to the letter of the ADT you made.
(The cruft includes source spans. I want to replace source spans with more detailed provenance. It also includes extensible Variants, which I wanted to use for precision of typing the implementation itself. Why can't we have nice things?? Blah blah blah)
So basically we need a way to handle source spans and similar stuff, without getting in the way of the rules we are writing down. The solution is pretty obvious, actually: we need our metatheory to care about metadata, so if we reuse the node it maintains the metadata, and if not it is forced to invent some new metadata for the node.
Similarly, we want unification to respect metadata in some way. So we need to allow non-linear pattern matching (this means reusing the same variable multiple times, and requiring that they are equal), and force some kind of unification algorithm to run, returning a unified object with aggregated metadata.
One of the philosophical things I want to push is that compiler errors should be associative, that they don't depend on the implementation of the type theory. And this requires rethinking monads and such. It's actually quite fun. But it requires a lot of foundational and linguistics work to make it easy to express, and fit into a coherent ecosystem.
This requires unification to be pretty lenient. In fact, the bad way to implement it would be to just keep all of the possibilities around, and deal with their coherence later. The better way is to think of what data structure and algorithm captures both their coherence and the nondeterminism.
(Really it should be a subtype in the sense of dependent type theory, but that's a bit much to ask of this sort of metatheory.)
-
Pie in the sky goal is that I wanted to try to get memoization of evaluation, based on sharing nodes. The features I talked about would already account for that – the compilation would be hard though, since it involves smuggling mutable data into immutable objects. It's difficult to say whether it would actually help performance (hint: the answer is probably no). But it would be cool to have a platform to make that experiment very easy.
-
The pie in the clouds goal is to have parsing be a first-class feature of the metatheory. Parsing is so cool when done right.
-
The pie in the stratosphere goal is that I want to have incremental computation in the mix too. Gosh that'd be so nice, for interactive AST editing. Can you imagine?? drools
I want to be able to write down both a paper theory, and have it just execute and run, and also a NbE theory. Yeah I really want to see NbE written down paper-style, since NbE is so cool and it would bring it full circle.
It's all about the right abstractions and the right language.
Really.
Lightweight syntax for powerful concepts.
It's a ton of work to build it, but I'm confident I can do it.
As long as I don't nerd snipe myself too much into the type theory of the metatheory, that is.
(Hint: I have an open tab searching for “regex containment algorithm” that is a serious idea I had for the type theory of the metatheory.)
Heck, I might just make it tactic-based and extensible. That'd be amazing, and easier to get started with.
(You know what tool would be good to implement my metatheory, right? ITSELF!)
Sorry again for the word geyser. I have a lot of deep ideas I've been slowly working on for almost 5 years now, too much to explain in depth here, but feel free to ask questions about it of course. That would allow me to write it out in chunks not all at once. <3
