has anyone ever researched/documented the interaction between encoding a large number of effects/dependent-types and API evolution? I'm concerned "usable" forms require lots of inference, which means lots of potential breaking changes to public APIs.
Conversation
Or even without inference, public APIs have to encode lots of incidental facts you wouldn't normally document that dramatically constrain the implementation.
2
4
Example in Rust: there's arguments for encoding: allocation, nounwind, simd (and which parts), float usage, atomic usage, i/o, purity, constexpr, thread-affinity, and probably others. This is a lot of things to guarantee/care about!
4
8
Not sure if you saw my retweet thread, but as I said there, I would assume changing effects should be a breaking API change anyway, but we're just getting away with it because it's not in our types at the moment:
Quote Tweet
Not sure if there has been any experience with adding and removing them. But then, shouldn't one be worried about that anyway if you are maintaining a library? While not specified by your types (without effects), they might inadvertently break your consumers anyway.
Show this thread
2
1
Eh, some effects are Very Niche but hoisting them to the type system suddenly makes everyone’s project stop building even if they don’t care about the niche effect
1
I would be interested to see how OCaml are planning to migrate to effects. Perhaps there are some ideas there. Not sure if they are just going to let things fragment though 🙄
2
2
Last I checked OCaml's algebraic effects were unchecked (just get a runtime exception if there's no handler in scope), with talk of -maybe- adding effect types later, not sure how far along they are with that?
1
Oh really? You mean the as-yet still being implemented stuff for multicore OCaml?
Yes as of last time I saw anything about it. But do look into it instead of taking my word because I'm not actively following it, just randomly see a thing here or a thing there :)
1