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
Yes, I think we're in agreement on all of that. I guess I'm just holding out hope that we can have a working theory of modularity without assuming K, univalence, or any other similar axioms, since otherwise Coq probably has to live with a broken module system forever...
1
1
I should really try to understand OTT, I suppose, maybe it is the most promising approach...
1
How does OTT (observational type theory I'm assuming?) relate to cubical type theory?