Or even without inference, public APIs have to encode lots of incidental facts you wouldn't normally document that dramatically constrain the implementation.
Conversation
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
One place you could look at is Java's checked exceptions, which have many failings due to their limited expressiveness, and are hence almost universally loathed. I wouldn't say that's reason to give up (much the opposite), but it might be useful to learn from what *not* to do.
1
Wrt. dependent types, proofs can often be broken in weird ways based on changes upstream, especially when based on tactic scripts. Maybe the Data61 and sel4 folks could give you more info there. AFAIK, they control most of their own code though. cc. , @cmrx64
1
1
Well that's a slightly separate issue, but yeah--besides the fact that tactic languages are often unprincipled (though not for Isabelle, I don't think?), modularity is kind of broken in dependent type theory... the values of constants tend to leak through in ways you can't avoid.
1
2
"modularity is kind of broken in dependent type theory" yeah - has there been any work done on trying to tackle this problem?
1
1
I'm not an expert in the subject, but I'm going to be asking an expert this very question today, since it's become a somewhat urgent matter in Coq... but my impression is that while work has been done, it has yet to arrive at a satisfying conclusion.
2
1
Oh cool. I've also noticed doing good docs for dependent types can be a pain. Like, sometimes Idris' docs sometimes will show some seemingly opaque type definition, but when you use it the internals leak out.
It would be nice to figure out what is public and what is private, for documentation, and print the definition along with the type if it's public... kind of a separate issue though.