| You're considering an alternative behavior for asymmetric fields in choices, but you need to consider the behavior of optional fields in choices too. In particular, the following duality is the lynchpin that ties everything together: "asymmetric" behaves like optional for struct readers and choice writers, but required for struct writers and choice readers. From that duality, the behavior of asymmetric fields is completely determined by the behavior of optional fields. It isn't up to us to decide arbitrarily. So the question becomes: what is the expected behavior of optional choice fields? Along the lines you proposed, one could try to make optional choice fields behave as if they had an uninhabited type, so that writers would be unable to instantiate them—then you get exactly the behavior you described for asymmetric choice fields. Optional fields are symmetric, so both readers and writers would treat them as the empty type. This satisfies the safety requirement, but only in a degenerate way: optional fields would then be completely useless. So this is not the way to go. It's important to take a step back and consider what "optional" ought to mean: optionality for a struct relaxes the burden on writers (they don't have to set the field), whereas for a choice the burden is relaxed on readers (they don't have to handle the field). So how do you allow readers to ignore a choice field? Not by refusing to construct it (which would make it useless), but rather by providing a fallback. So the insight is not to think of optional as a type operator (1 + T) that should be dualised in some way (0 * T), but rather to think about the requirements imposed on writers and readers. You're right to note the duality between sums and products and initial and terminal objects, and indeed category theory had a strong influence on Typical's design. |