Just foxing about.
Comment by ~icefox on ~icefox/garnet
It's certainly in the general region of the design space, though I kinda want to avoid them if I can simply for the sake of Garnet's "don't be a research project" goal -- which I may have already failed by now, admittedly. My thoughts on effects in general are in the first couple sections on https://man.sr.ht/~icefox/garnet/properties.md, so that's probably something like what you saw. I haven't looked much at Effekt though, that sounds like something I should do.
My main beef with effects as usually discussed in Academic Things is that they really like their non-local control flow, and I really would like to avoid that as much as I can for Garnet. It makes borrow checking hard, it makes reasoning about programs hard (or litters your programs with annotations), it makes your compiler more complicated (a la Rust async), and so on. If I wanted a unification of non-local control flow I'd already have Lua-like coroutines, but decided not to for basically those reasons. It's a great solution for a managed language that is not Garnet.
However... I might see what you're getting at. Threads already involve non-local control flow so using property-like things to manage their effects could be interesting. Beyond only just applying to functions you could make threads that have properties like "doesn't panic" or "can't leak resources" or such, which could be pretty useful...
Hi ~icefox, not sure if it is at all in the design space you are going for, but exceptions as algebraic effects is definitely another strategy. I saw somewhere on your wiki that you had looked into Koka - I think Koka is neat, but kind of hard to learn how algebraic effects work from (definitely for the reasons you outlined there - wrt. koka's model being non-local control flow and side-effects tracking smushed together). If you're interested in getting a handle on them if you don't have one already, I really recommend checking out the Effekt language and their language design papers, I found them way easier to read than the Koka ones: https://effekt-lang.org/publications.html
The concrete benefit of an algebraic effects approach to exceptions is because algebraic effects are a unification of all non-local control flow, you get reasonable semantics around their interactions with threading and async and freeing things for-free. You would very likely lose out on some performance though, and how to make syntax around algebraic effects reasonably understandable still seems to be a work in progress for sure. This would also let you convert between values as errors (Result[T, E] etc) and exceptions as errors (raise E) fairly easily, but you could do that without an algebraic effects system - I think Swift has some interesting work in the design space around this with their try stuff, that I think Rust has been working on stealing.
Also, algebraic effects would allow you to assert a function does not panic. In the system of Effekt all effects aside from those on first-class functions are inferred. But you can assert a function to be pure by appending
/ ()(or something along those lines - forget the exact syntax) after the type. You could also definitely do this with just a side effect tracking system, though.
Comment by ~icefox on ~icefox/garnet
Here we go, this will be useful: https://smlfamily.github.io/Basis/overview.html Probably outdated, but useful.
Comment by ~icefox on ~icefox/garnet
Zig looks worth learning from: https://andrewkelley.me/post/zig-stack-traces-kernel-panic-bare-bones-os.html
Comment by ~icefox on ~icefox/garnet
Aha, the "GCC Runtime Library Exception" appears to be basically the formalization of what I want: https://www.gnu.org/licenses/gcc-exception-3.1.html The language and terminology is kinda a pedantic pain in the ass, like GPL 3's language is, but it's also maintained by GNU and probably will be for the forseeable future so it's probably the canonical choice. The GNAT Ada compiler uses it, and has a paid variant with lawyers standing behind it, so it's probably been vetted pretty thoroughly. Still needs closer inspection though.
Comment by ~icefox on ~icefox/garnet
I've finally sat down and proven you can totally make a safe-but-limited borrow checker, with a couple relatively simple invariants: references may not live on the heap, and references on the stack may only point at things longer-lived than they are -- ie, they may only point up the call stack. It's not quite trivial, you have to make sure mutable references aren't mutated to point to something younger than themselves. But it seems like a good first step.
Comment by ~icefox on ~icefox/garnet
Yeah an ABI is always gonna be a backwards compat issue, one way or another. Just look at Windows and all the things in it that can never be fixed. But it's also a gateway to... well, everything; just look at all the Rust libraries out there that have to present a C-like API to let other languages use them, and all the C++ libraries out there that can never be used from other languages 'cause they can't instantiate templates. Saying "we don't need an ABI" is one of those things where if you don't have it then people will re-invent it anyway, badly.
I vaguely remember reading something like along the lines of "we don't need a stable ABI" as well, maybe it was this? https://blaz.is/blog/post/we-dont-need-a-stable-abi/ Upon actually reading that though, it's a lot more moderate than the title makes it sound, I more or less agree that "runtime type info" is the way to go.
More references from Rust:
- Rust
crabiproposal: https://github.com/rust-lang/rust/issues/111423stabby: https://lib.rs/crates/stabbysabi: https://lib.rs/crates/abi_stable- uh, general purpose info I guess? https://slightknack.github.io/rust-abi-wiki/
By now I've been sorta low-key assuming that no language more complicated than C will have a perfect mapping to any ABI (and C isn't exactly low-complexity anyway). But instead of making a "Garnet ABI" that expresses everything Garnet does perfectly, it might be best to have a sorta least-common-denominator that is nonetheless more powerful than the existing least-common-denominator of C. The circle-lang link kinda takes a similar approach, trying to describe the most useful things instead of everything. It can have rules for expressing things like "can this function unwind or not", "is this value moved or borrowed", "is this value
Copy", stuff like that, so a compiler and linker have more information to work with about how to lego together bits of code.