These remind me of type driven development with holes. It’s not quite the same, since you aren’t really “running” parts of the program, instead you write typed definitions that might have some holes and the type system tells you what the type of the expression in the hole should be. Edwin Brady has mentioned that he’d love to see someone build a Smalltalk style system on top of Idris, and I concur. It would be really interesting to see the safety of quantiative type theory (that just means some variables are linear) combined with the interactivity of Lisps.

The propagation of modified struct definitions is an interesting challenge, it sounds like database migrations. I’m actually skeptical if a language with neither type inference nor type annotations could deduce what to do with a struct change. Just because a type has a default value does not mean that it’s the correct one to use in a struct. Even if we restrict it to just be the “neutral” element, if you’ve studied some group theory you know that that is not determined by the type (the set) but the operations you use on it. Addition and multiplication have different neutral elements. I think cubical types could be used here, but that’s just a hunch. If you have a well defined equality relation between the old type and the new, then a sufficiently smart runtime could rewrite all instances in-memory.

Another sticky issue is how this interacts with multiple threads. Would just pausing them during the rewrite be enough?

🤔