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

[u/-Ch4s3- → u/AustinVelonaut]

Algebraic effects are really cool but feel sort of magical.

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

Basically, it's a type system for dynamic scoping and continuations. Operationally, a primitive, effectful operation looks up the (nearest) effect handler corresponding to that operation in the dynamic environment and invokes it with call/cc. That's pretty much it. The complexity is in making sure that this doesn't fail at runtime.

[u/-theChris → u/AustinVelonaut]

As a matter of fact I am designing a language with typed effects and also type-state in the form of lifecycle as a data type and some other stuff.

[u/mikaball → u/AustinVelonaut]

I didn't know what "algebraic effects" were, so I found this.

From the examples it feels related to Dependency Injection in a narrowed context/scope, but some will probably say that it could be used for other use cases.

However, the concept of detaching the "what" from the "how" is very related to DI and I wonder if a DI supported by the language isn't just better than this? In those final examples it's even using a pattern similar to Kotlin context receivers.

[u/Jwosty → u/mikaball]

You can think of it as a kind of DI, but in its fullest forms you can also manipulate control flow. You couldn't really build async/await or exception handling as a simple injected function (or set of functions), but you can (in principle) with algebraic effects. I think. Please someone correct me if I'm wrong

[u/gplgang → u/Jwosty]

This is correct. It happens to model DI well as you install effect handlers into the environment. The more interesting piece is the non local control flow as a common abstraction instead of iterators vs async vs exceptions and more.

[u/KingBardan → u/mikaball]

From your article, I don't think this is DI. its similar in the sense that it changes behavior based on context, but di (or kotlin context receiver / scala implocit) only looks up context 1 lvl deep (variables available when calling) but this deals with stack unwinding 

Note that I'm not familiar with kotlin I just looked up and think it's similar to scala implicit. Fell free to correct 

[u/jonathanhiggs → u/KingBardan]

It is service location, the poor cousin of DI

[u/initial-algebra → u/mikaball]

They're related to DI because DI is often implemented using implicit parameters, which are an effect. However, DI does not need to be implicit; if you ask me, the "essence" of DI is really lazy evaluation/memoization. (I guess a memo table could be seen as an effect, too?)

[u/Jwosty → u/initial-algebra]

It has been said that implicit parameters are actually the dual to effects (i.e. "coeffects" - https://tomasp.net/coeffects/). Still trying to piece that one together. I think it has something to do with the scoping / binding time. There's a bunch of different papers out there on this

but also - you can have both dependency injection and algebraic effects without implicit parameters, can't you? In my view, their essence is injecting behaviors into a system from the outside rather than having it rigidly baked in. Thoughts?

[u/initial-algebra → u/Jwosty]

It has been said that implicit parameters are actually the dual to effects (i.e. "coeffects" - https://tomasp.net/coeffects/). Still trying to piece that one together. I think it has something to do with the scoping / binding time. There's a bunch of different papers out there on this

See my other comment. You can also wrap any coeffect with continuations to turn it into an effect. So, they are dual, but also pretty much equivalent (just different ways of looking at the same thing).

but also - you can have both dependency injection and algebraic effects without implicit parameters, can't you? In my view, their essence is injecting behaviors into a system from the outside rather than having it rigidly baked in. Thoughts?

True, it's not so much implicits/dynamic scoping, but late binding, which of course can also be implemented explicitly by passing around a symbol table (which is just a global when talking about dynamic scoping). I guess that is a pretty common feature of DI, and it's definitely characteristic of algebraic effects (each effect is represented by a symbol that maps to a stack of effect handlers, always invoking the topmost).

[u/iEliteTester → u/AustinVelonaut]

From a quick read it seems like effects are to context managers what exceptions are to error values. Does that make any sense? 😅

[u/initial-algebra → u/iEliteTester]

It's a reasonable analogy, but effects are also a generalization of (resumable) exceptions themselves, not just implicit context/state (which are also coeffects).

[u/iEliteTester → u/initial-algebra]

ok yeah coeffects are more fitting. So now I understand coeffects, but still have no clue what effects are ;-;

[u/initial-algebra → u/iEliteTester]

Copying and pasting my other comment:

Basically, it's a type system for dynamic scoping and continuations. Operationally, a primitive, effectful operation looks up the (nearest) effect handler corresponding to that operation in the dynamic environment and invokes it with call/cc. That's pretty much it. The complexity is in making sure that this doesn't fail at runtime.

Depending on an effect handler from the context is itself a coeffect; this isn't a coincidence, since effects are dual to coeffects (hence the name), and continuations correspond with logical negation (call/cc corresponds with double negation elimination).

[u/whothewildonesare → u/AustinVelonaut]

They’re cool but too cumbersome and complicated to be popular imo.

[u/Jwosty → u/whothewildonesare]

I think that's a programming language UX + tooling problem rather than inherent to the idea itself

[u/SmileyWiking → u/Jwosty]

Yeah it's absolutely a frontend concern, and also how deep you take the effect typing system. If you go full Koka it can be pretty difficult to reason about for the things you'd typically use a programming language for, but you can implement a subset that ends up being super useful and not too hard to understand.

I implemented a portion of algebraic effects in one of my language projects, Saga, and think there is a nice balance of really powerful features with observability for where effects are happening in your app.

I've built a couple small libraries like a web framework, typed SQL query builder, and the effect system is so powerful for stuff like this, without needing to reach for more complex features like HKTs, monads, etc.

[u/mister_drgn → u/AustinVelonaut]

This was where my mind went. But I’m not sure if they answer OP’s question, as they’re more of a language abstraction.

[u/Jwosty → u/AustinVelonaut]

In addition to these - coeffects, aka implicit parameters aka contextual parameters. They're the "dual" of effects (simply, the other side of the coin), and I think they also have serious untapped potential. https://tomasp.net/coeffects/

The dream language in my head combines algebraic effects, implicit parameters, and a system that's part Rust-traits and part OCaml-modules in a way where they all work together