jfecher's comments

jfecher | 6 months ago | on: Group Borrowing: Zero-cost memory safety with fewer restrictions

> 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.

jfecher | 10 months ago | on: Why Algebraic Effects?

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"

jfecher | 10 months ago | on: Why Algebraic Effects?

> 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.

jfecher | 10 months ago | on: Why Algebraic Effects?

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.

jfecher | 10 months ago | on: Why Algebraic Effects?

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.

jfecher | 10 months ago | on: Why Algebraic Effects?

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.

jfecher | 2 years ago | on: Algebraic effects, ownership, and borrowing

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.

jfecher | 2 years ago | on: Algebraic effects, ownership, and borrowing

Hi, author here!

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.

jfecher | 3 years ago | on: Ante: A low-level functional language

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`.

jfecher | 3 years ago | on: Ante: A low-level functional language

C can sometimes be an easier target since you don't have to learn LLVM's API. C is also more portable than llvm since there is a greater variety of C compilers for a greater variety of architectures than llvm targets.

jfecher | 3 years ago | on: Ante: A low-level functional language

Ack, my apologies, I didn't intend to be so inflammatory! If memory serves AFL was one of the first schemes (or perhaps the first?) to abandon the stack discipline to provide better inference in quite a few cases compared to TT. I remember the graphs in that paper giving me more hope for region inference to be a practical memory management scheme. Later, I believe the imperative regions paper improved on the AFL scheme a bit at least in their single 'life' example, but without more test cases or graphs it is more difficult in general to assess that paper or how common this case matters in practice. I'm curious what you believe the future of research for region inference to be considering most of the papers written after TT's retrospective paper seem to have moved in the direction of explicit regions rather than inferred ones.

jfecher | 3 years ago | on: Ante: A low-level functional language

This is definitely an issue, but isn't one I run into often. Just like if I'm pasting code in rust I need to make sure it is inside or outside an if statement, I likewise need to ensure pasted code in ante is inside/outside the if statement by looking at its indentation relative to the previous line. The compiler can help somewhat here, just not a lot. If your indentation is not on an existing indentation level you will get an error since you cannot randomly start indent blocks in your code. I do think the biggest detractor of indentation-sensitive syntax in general is the loss of auto-formatting indentation though.

jfecher | 3 years ago | on: Ante: A low-level functional language

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.

jfecher | 3 years ago | on: Ante: A low-level functional language

My definition of low level is no tracing GC, values are unboxed by default, and users still have control to do low level things (raw pointers, other unsafe operations) when needed, even if it is not the default.

jfecher | 3 years ago | on: Ante: A low-level functional language

Correct, a key goal is to have no explicit region/lifetime annotations. There have been several papers on region inference after the originals by Tofte & Taplin, all attempting to refine the original analysis by inferring shorter lifetimes. First by analyzing when a region can be safely emptied and re-used, then by abandoning the stack discipline, etc. Unfortunately, none of these are viable in a real program in my opinion. Although they each infer shorter lifetimes in a few cases the core problem of "collections will unify the lifetime variables of all elements in the collection" and "branching on a value and conditionally returning it extends its lifetime, even if the branch was not taken" remain unsolved.

An ideal solution to me needs to solve these problems. Since there is already a large body of research trying to address this on the static side and failing, I believe it needs to be solved with runtime checks. The specifics of which I'm still exploring but its worth mentioning these would only be necessary to tighten existing lifetimes so one can envision annotations or compiler options to elide these if desired. Lifetime inference in MLKit (and I believe ante as well) tends to speed things up by turning more dynamic allocations into stack allocations, so there is some room there for runtime checks without making the result more expensive than the version with dynamic allocation I believe.

jfecher | 3 years ago | on: Ante: A low-level functional language

This is definitely an interesting thought. My thinking is that "the fun stuff" tends to help make the language more functional, so removing it you are left with a more imperative language resembling a C clone with traits and type inference. Then if you want easier C interop you must remove traits and either remove modules as well or provide a standard method of mangling module names into function names. At that point I think you may as well use an existing "better C" language like Odin, Zig, Jai, C3, etc.

jfecher | 3 years ago | on: Ante: A low-level functional language

Author here, thank you for your interest! There are definitely a lot of small design decisions that add up in language design, from using `|` for match cases to avoid double-indentation, to the use of pairs over tuples, to how methods are resolved and chained, it is nice to have others appreciate the small things sometimes :).

I'll avoid posting it here but if you do want to follow ante's development the best place is on its discord which is linked on the github page.

jfecher | 3 years ago | on: Ante: A low-level functional language

More or less, yes. I may later change it to some type like `Interpolated env` to represent a lazily interpreted string that interpolates the types in env. So "${1u8} and ${2}" would be typed as Interpolated (u8, i32).

I'd like to keep this orthogonal to IO or other specific use cases so that it is applicable to any use case users may have rather than tailored to existing ones. You're also correct there is no real logging framework or anything of the kind except print really. Ante is still in a quite early state and there aren't really any substantial libraries to speak of. As-is, interpolation is really just some nice sugar to make some common operations more ergonomic, like f-strings in python.

I think applications that need their own dynamic interpolation requirements should define their own interpolation to handle their specific needs. It would be unacceptable from a performance and predictability standpoint for example to support the example of loading files into a string and have them interpolated at runtime automatically for all file loads.

jfecher | 3 years ago | on: Ante: A low-level functional language

(1): No support, some monad or early-error-return sugar used to be considered but effects cover most of the usecases of monads and are easier to use so I plan on emphasizing them. As for arrows, I have to say here that I've actually never used them in haskell so I don't know how useful they'd be.

(2): Thanks for the resource, I'll look it over :). I remember seeing a vaguely related note that multicore OCaml used to provide a `Obj.clone_continuation` function but no longer does. Of course, ante's algebraic effects design is rather different so that may not apply anyway. It may depend on the Generator whether it is cloneable or not. Some generators are just functions that can be arbitrarily cloned, but others are closures which may have restrictions in whether their environment is cloneable. Ante's clone story in general needs more work.

page 1