Description
I was discussing best practices with Egbert yesterday (in person!) and in particular what lessons from my background would be applicable and valuable to agda-unimath. (For context, in my professional life I am one of three people with decision-making authority over best practices for one of the most-used languages in Google's codebase, and my team as a whole has authority over another.)
At the top of my list was encapsulation, in the restriction-of-access sense, and its implications for easing refactoring work. There are a number of potential applications we discussed -- the definition of polynomials at the top of the list -- but in this issue I will give an example that exists in the codebase today: the definition of positivity of a rational number.
Currently, this is defined as the positivity of the numerator, but there are certainly equivalent formulations, some of which are proved in the library -- most notably, zero-Q being strictly less than the rational number. Egbert has already mentioned interest in overhauling elementary number theory, including potentially redesigning the rational numbers. Fundamentally, the question is what best practices might minimize the amount of effort involved in making such changes?
Software engineering has a clear and specific answer, encapsulation, which in this particular instance I would apply by making the definition of is-positive-Q opaque, or making the entire file abstract. Instead of pattern-matching, or getting out the semantic content of the is-positive-Q witness (the positivity of the numerator), access should be done through functions as frequently as possible. Within the same file, within elementary-number-theory/positive-rational-numbers.lagda.md, code should feel free to unfold that opaque definition or be within the abstract block, but that should be minimized or even forbidden outside of the file.
The objective, in particular, is that if we need to change the internal content of is-positive-Q -- which definition of positivity is used -- that should only entail changes within that same file where it is defined, not across every use site.
The general guideline of encapsulation is probably to make things abstract, or at least opaque, by default -- unless there is a compelling reason otherwise, which is weighed against the expected cost of "we have to change this around later and change all the use sites accordingly." That expected value is affected by both our estimate of the likelihood of future change and the associated effort.
Egbert certainly seemed interested in this practice, but I'll let him weigh in with his own thoughts. Additionally, it's worth discussing that getting the existing agda-unimath codebase to abide by this practice would be a significant amount of work, incrementally requiring the abstraction of more and more of the library.