> I'm actually hoping to find a way to blend Nick's approach seamlessly with reference counting (preferably without risking panics or deadlocks) to get the best of both worlds, so that we can consider it for Mojo. I consider that the holy grail of memory safety, and some recent developments give me some hope for that!
Ante's approach manages to blend a similar scheme for safe, shared mutability with Rc. There are some examples on the most recent blog post on its website of it. IMO combined with its shared types it emulates high-level GC'd code very well.
Right, compared to explicitly passing the parameter, with effects:
- You wouldn't have to edit the body of the function to thread through the parameter.
- The `can Use Strings` part can be inferred (and in Ante's case, it is my goal to have the compiler write in inferred types for you so that top-level definitions can be inferred if desired but still annotated when committed for code review).
- Most notably, the `can Use Strings` can be included in a type alias. You could have an alias `MyEffects = can Use Strings, Throw FooError`, etc for the effects commonly used in your program. If your state type is used pervasively throughout, this could be a good option. When you have such an alias it also means you'd just be editing the alias rather than every function individually.
Generally though, while I think the passing around of state through effects can be useful it isn't the most convincing use of effects. I mention it more for "here's another benefit they can have" rather than "here's this amazing reason you should definitely use them for"
> Generally though, while I think the passing around of state through effects can be useful it isn't the most convincing use of effects.
I actually find it quite convincing, even if it might not be the main use case. Nowadays in imperative languages there are countless popular frameworks that resort to using & manipulating global state behind the scenes because drilling context through the call stack by hand is painful. Unfortunately, this makes understanding code much more difficult and testing it even more so.
> As I understand it, AE on low level is implemented as a longjmp instruction with register handling (so you can resume).
Not quite. setjmp/lonjmp as they exist in C at least can jump up the call stack but not back down. I mention this at the end of the article but each language implements algebraic effects differently, and efficiency has improved in recent years. Languages can also optimize the effect differently based on how the handler is defined:
- Handlers which are tail-resumptive can implement the effect as a normal closure call.
- Handlers which don't call resume can be implemented as an exception or just return an error value at every step until the function exits the handler.
- Handlers which perform work after resume is called (e.g. `| my_effect x -> foo (); resume (); bar ()` can be implemented with e.g. segmented call stacks.
- Handlers where resume is called multiple times need an equivalent of a delimited continuation.
Another way to implement these generally is to transform the effects into monads. For any set of effects you can translate it into a monad transformer where each effect is its own monad, or the free monad can be used as well. The cost in this approach is often from boxing closures passed to the bind function.
Koka has its own approach where it translates effects to capability passing then bubbles them up to the handler (returns an error value until it gets to the handler).
With just a few restrictions you can even specialize effects & handlers out of the program completely. This is what Effekt does.
There really are a lot of options here. I have some links at the end of the article in the foot notes on papers for Koka and Effekt that implement the approaches above if you're interested.
If the database effect wrote to a file it'd require the `IO` effect and code using it would need that effect as well. A compiler can generally show a function to be free of most side effects if it uses no effects. The exceptions to this are things like divergence. As long as the language is Turing complete you can't prove it won't loop forever of course. Another exception could be extern functions which the compiler can't verify the correctness of the type signature. Different languages handle these differently but if users are allowed to write any (and the language doesn't force them to have an IO effect) then they can be a source of unsafety. Languages like Koka and Effekt are considered pure though and enforce this through their effect systems.
Developer of Ante here. Functions in languages with effect systems are usually effect polymorphic. You can see the example in the article of a polymorphic map function which accepts functions performing any effect(s) including no effect(s). For this reason effect systems are one of the solutions to the "what color is your function" problem.
Author of Ante here - it actually already has an (extremely basic) LSP. Tooling more or less required for new languages out of the gate these days and I'm eyeing the debugging experience too to see if I can get replayability at least in debug mode by default.
Ante is still mostly unusable unfortunately! Ownership & Borrowing were a relatively recent change and I've still yet to implement them. Algebraic effects are also still in progress in a dev branch and won't be merged for some time. You can use the language today but it will feel more like C with traits, generics, and bugs rather than a more featureful language.
The language does have a basic language server already though! It currently supports inline diagnostics and hover to show type.
If anyone's curious, here's how ante addresses these issues:
- It causes memory unsafety: Ante's `shared` references prevent memory unsafety by preventing projecting them into "shape-unstable" types like a vector's element
- Iterator invalidation: This is the previous point in disguise. Since iterating over a shared vector would grab references to its elements - this is prevented since it is shape-unstable. You'd need to clone the elements.
- It's effectively threaded: This is the same bug yet again! Once shared-ness is tracked this becomes a non-issue. Ante is still able to have the static guarantee that this can't happen but does not need to prevent sharing to do so.
- Safe Abstractions: This section is a bit general but it's worth noting Ante still has the ability to have `&own mut t` references if needed. The `swap` function there could use them for example.
Overall the claim that "Aliasing that doesn’t fit the RWLock pattern is dangerous" is fairly rust-centric. It would be dangerous if you had no other restrictions, but we could also adopt different restrictions that still permit aliasing but disallow projection into shape-unstable types instead.
Hi! An uninterpreted function is one where the only thing we can assume about it is that `(x = y) => (f x = f y)`. That is if we give it the same input, we should get the same result out. In the context of refinement types this can be used for, among other things, tagging values with some predicate.
For example, if we know `good_index array 3` and `x = 3` then we know `good_index array x`.
Lifetime inference originates from region inference which is actually completely unrelated to linear/affine/uniqueness typing. Uniqueness typing can definitely complement lifetime inference, but isn't really generalizeable to it.
Ante's approach manages to blend a similar scheme for safe, shared mutability with Rc. There are some examples on the most recent blog post on its website of it. IMO combined with its shared types it emulates high-level GC'd code very well.