This is an automated archive made by the Lemmit Bot.

The original was posted on /r/programminglanguages by /u/ebingdom on 2024-03-23 10:53:51.

What is the state of the art in combining dependent types and side effects like divergence, partiality, mutable state, etc.? I recall coming across some papers over the years with various ways of tracking which code is “pure” in types or contexts (or universes or kinds or …), and allowing impure programs to occur in types only in controlled situations (so that you can still write proofs about impure programs, but you can’t use impure programs to produce bogus proofs). Another challenge is writing polymorphic code that can be reused in both proofs and programs to avoid duplication (such as pairing/projections and other general purpose facilities). Is there a satisfying solution or is more research needed? Does call-by-push value help with this somehow?

(To clarify, I am asking about side effects, not computational effects in general.)