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
Yeah, still getting to grips with regular ol' dependent type theory! I am starting to see though how annoying equality can be though! Super exciting to see the progress the on cubical front, even if it is still a bit beyond me!