IntersectMBO
Should we use dependent sum and product types visibly?
We should first try to assess the necessity for this. So the questions to ask are:
- where do we actually show dependent function and product types in the PDF, and
- do we actually need to show them?
By the second item, I don't necessarily mean to just hide them. It can also mean to refactor the code to remove it completely. Once we have this information, we can then make an assessment: what's the cost of not using these (for us and our audience), versus the cost of having to read a tutorial on it?
Dependent sum and product types came up twice recently:
- For
KeyPair(a dependent sum type), which is only ever used in expressing properties of crypto primitives. I think this can be refactored at quite a low cost. - For defining our own universes, e.g. here: https://github.com/IntersectMBO/formal-ledger-specifications/issues/130.
Are there any other instances of dependent pairs that would be more difficult to get rid of?
If we end up using universes for something, I don't think we need to fully explain dependent products. An explanation that covers the situation we're interested in would be sufficient and probably much easier for a novice.
Explanations could use #276 as a starting point.
