Miss Dada  🏳️‍⚧️

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.

Or even without inference, public APIs have to encode lots of incidental facts you wouldn't normally document that dramatically constrain the implementation.

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!

I vaguely lean towards the C answer here. Public API is what's documented. I `#[nodoc]` everything I don't want to be relied on (and in rare cases just mention in the docs "you shouldn't rely on X"). Of course you still have to consider "does this actually break code" on changes

right but I'm specifically talking about a world where everyone wants you to interoperate with dozens of (potentially adhoc) effects. Every effect you incidentally satisfy that you refuse to document makes your library less useful.

Yup, this is the world I live in. I think it's easy to over-estimate how bad it is, as long as you actively consider "what realistically could break" with every change, and take the spirit of RFC 1105 to heart.

Do you think this philosophy would be tractable in a world of pervasive dependent typing?

I don't know that I can give a better answer than "it depends". Maybe you should ask an Idris programmer. ;) For Diesel we work around this by "the public API for the result of this method is this helper type w/ the same name". Associated type values are generally private