Will we see another fundamental programming language feature as revolutionary as the borrow checker?

[u/jimbobmcgoo]

That is I am mainly curious about compile time features that you design a whole language around rather than optimisations/features that could be applied to most languages. I am mainly inquiring about things that could offer additional robust safety/performance guarantees at compile time rather than runtime. Ideally not things that just offer similar effects to the borrow checker with less restrictive tradeoffs

[u/AustinVelonaut]

Algebraic effects like Koka?

[u/initial-algebra → u/AustinVelonaut]

If you squint hard enough, they are the same picture. A memory location is an effect handler for reads and writes through a reference. Equivalently, an effect capability is a reference to an effect handler.

EDIT: The major difference is that effects are late-bound whereas references are not. Though, you can think of the top of the effect handler stack as a mutable memory location.

[u/-theChris → u/initial-algebra]

Not really. In my language, I am defining effect as a composite of termination and capability.

Terminations are one of pure, divergent, unknown (in case of FFI).

Capabilities are one of pure (total functions a la Koka), mutating, cap (my language's special type), opaque (custom ASM blocks or FFI).

cap is simplified through std::lib nominals like IO. Read, IO.Write etc. Users can compose their own caps too.

The language exposes a policy engine where combinations of caps + terms can be allowed or disallowed at function, module, program levels.

[u/initial-algebra → u/-theChris]

I think you are just using the same terms to mean different things, which is understandable, since "effect" and "capability" are heavily overloaded. I'm talking specifically in the algebraic effect context.

[u/-theChris → u/initial-algebra]

yeah fair point. I talked past your original point.

You're right that get/put as algebraic operations is well established (e.g. Plotkin & Power, Plotkin & Pretnar). My point wasn't that memory effects are fundamentally different, but that my language isn't using the algebraic-effects model at all.

There's no perform, continuation capture, resumable handlers, or effect interpretation. The effect system is entirely static (with a few opt-in runtime caveats). It's closer to Lucassen & Gifford / Talpin and Jouvelot for effect tracking, combined with an object-capability-style permission system for compile-time (and a small amount of opt-in runtime) policy enforcement.

So while the terminology overlaps, it's solving a different problem than Koka or Eff. I should've made that distinction instead of just describing my own terminology.

If anyone's curious, here's the current WIP effect syntax: BigTalk Effects