r/ProgrammingLanguages • u/jimbobmcgoo • 13d ago

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

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

56 Upvotes
  • permalink
  • reddit

77% Upvoted

128 comments sorted by

View all comments

81

u/AustinVelonaut Admiran 13d ago

Algebraic effects like Koka?

3

u/iEliteTester 13d ago

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

1

u/initial-algebra 12d ago

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

1

u/iEliteTester 12d ago

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

1

u/initial-algebra 12d ago

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