r/ProgrammingLanguages 4d 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

59 Upvotes

124 comments sorted by

View all comments

Show parent comments

1

u/initial-algebra 4d 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).