using System
using System (c0, c1, c2, ...)
using ε = System (c0, c1, c2, ...)
using ε = System (c0 = c0, c1 = c1, c2 = c2, ...)
using Sys = System (p = print)
@"""A multiline docstring for a file"""
def f =
@"this is the fabulous 'f' combinator"
[X -> 42]
>> help 'f'
{"this is the fabulous 'f' combinator"}
~VMObjectArray() {
#ifdef GC_STOPGAP
if (deferring) {
for (int i = 0; i < _size; i++) {
defer.push(_array[i]);
}
delete[] _array;
} else {
deferring = true;
for (int i = 0; i < _size; i++) {
defer.push(_array[i]);
}
delete[] _array;
while (!defer.empty()) {
defer.pop();
}
deferring = false;
}
#else
delete[] _array;
#endif
}
Egel runtime objects are instances of C++'s std::shared_ptr. Because egel objects can be deeply nested, it is not uncommon for large structures to go out of scope and result in cascading frees that blow up the C stack.
I.e., the following short egel program would core dump:
# rewrite a list of a million numbers to none
from_to 0 1000000 |> [_ -> none]
class GC {
public:
GC() {
}
void push(const VMObjectPtr &o) {
std::lock_guard<std::mutex> lock(mtx_in);
_in.push(o);
}
void copy() {
std::scoped_lock lock(mtx_in, mtx_out);
while (!_in.empty()) {
_out.push(_in.top());
_in.pop();
}
}
bool done() {
std::scoped_lock lock(mtx_in, mtx_out);
return _in.empty() && _out.empty();
}
void empty() {
std::lock_guard<std::mutex> lock(mtx_out);
while (!_out.empty()) _out.pop();
}
void clear() {
while (!done()) {
copy();
empty();
}
}
private:
mutable std::mutex mtx_in;
mutable std::mutex mtx_out;
std::stack<vmobjectptr> _in;
std::stack<vmobjectptr> _out;
};
inline GC garbage_collector;
~VMObjectArray() {
for (int i = 0; i < _size; i++) {
garbage_collector.push(_array[i]);
}
delete[] _array;
}
while ((trampoline != nullptr) && (*run != HALTED)) {
if (*run == RUNNING) {
trampoline = f->reduce(trampoline);
garbage_collector.clear();
} else if (*run == SLEEPING) {
std::this_thread::sleep_for(std::chrono::milliseconds(100));
} else { // *run == HALTED
}
}
I wanted to show that Egel can be used to create small tools, and decided upon a temporal logic synthesizer. After reading a bit I trimmed that down to: do something useful with LTL and Z3. The first because LTL is relatively small, the latter since I want Z3 bindings for Advent of Code anyway.
Synthesis is a bit of a hopeless subject since the best you can hope for is to derive small automata with maybe five states. Moreover, it already exploded on translating LTL to negation normal form, the first ostensibly minor step in the whole process.
But I remain committed for now.
Some people pointed me at E-graphs, a manner for representing and then heuristically minimizing terms. Of course, Boolean circuits are terms too and minimizing circuits is PSPACE. Very much so, even.
So, it's unclear how much minimization you can actually achieve with E-graphs.
Two forms (b?f:g)(x) and f(b?x:y), should be enough for all (functional) control flow analysis. In a very abstract sense, application and choice are all you need.
Of course, you just need a rewrite to a term that uses b0? f(b1?x:y) : g foo to see that 'f' is still hoisted. But it won't be pretty so that's an issue.
(b?f:g)(x)
Tongue in cheek, of course. Control flow corresponds to determining what (part of a) program you will run next and, of course, you can always compile down to lambda calculus in an abstract sense.
Those who have watched the critically acclaimed "Egel - The Movie" (8 upvotes on lobste.rs) know that I've been dabbling with a small rewriter with a trivialized semantics. The observant viewer might have noticed an off-the-cuff remark in that movie that Egel, since it rewrites, has less need for tail-call optimization, some stuff comes for free.
Let's revisit a small recursive function, factorial: fac 1 = 1 | fac n = n * fac (n-1).
Those who know some compiler theory will know the runtime behaviour of that function if implemented according to the Algol convention for stack machines: for every invocation, a stack frame is created with a dynamic and static link and some space for local variables. The program will subsequently perform its operations within the context of that frame, and for each recursive call, a new stackframe is pushed to the stack.
Egel in contrast, will rewrite a redex to another number of redexes. For a stack machine that corresponds to removing the callee's stack frame entirely and pushing several stack frames with work to be done to the stack. Hence my remark that there's less need for tail-call optimization, for simple recursive functions that consume constant stack space you get that for free. Also noteworthy, tail-call optimization module cons comes for free too.
And that begs the question of whether other calling conventions are wrong, at least for ML-like languages.
using System
data tick
def do_tick = [K -> throw (tick K)]
def handle_tick = [N (tick K) -> try K N catch handle_tick (N+1)]
def main = try do_tick [N -> do_tick ((+) N)] catch handle_tick 1
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.
