I saw give a really good description of the frustrations over choosing parameters vs. fields in (when designing APIs for ML-style module systems) in his interview with :
Conversation
“…when you have a component you don't know how many things to parameterise it by. Do you want to parameterise it by the type of strings, or date-times? You could do that! But by doing that you make the component more complex, and you've got to make all the choices up-front.“
1
3
I also run into similar issues with Rust's traits - where you might want to let the clients of an API customise types for efficiency, either with parameters or associated types… but that can make the API overwhelmingly complicated and prevents the use of dynamic dispatch.
1
2
I think this is related to the ’bundling problem‘ - where you need to decide up front whether to use fields or parameters, that 's work has been tackling:
1
4
Why3 also has some fun ways of approaching this issue with its approach to ‘module cloning‘, where you can take an existing module with abstract or concretely defined fields, and substitute them for other definitions: why3.lri.fr/doc/syntaxref.
Replying to
I think Arend also has a cool way to partially 'fill up' the fields of records, which I think is a pretty neat approach? Can never really remember where in the docs it is documented though.
2
7
Always interested in learning about other approaches to this issue, and if there are any other ideas for integrating this stuff ergonomically into dependently typed module systems!
3