The central building block is a positive, divisible-by-10 integer (equivalently, a natural number of digits for a base-10 number), e.g. 10000 --> 4. This would have type something like type UpperBound <: Singleton & PositiveInt, and then the values passed for representation would have type something like n: Int :| Greater[0] & Less[UpperBound]. This would facilitate, then, typesafe encoding of integers for things like field of view, timepoint, and imaging channel, with the number of characters encoding the number equal to the number of base-10 digits needed to encode the subdomain's max value (e.g. 4 for 9999 < 10000).
As an even further generalisation, the base of the upper bound of the subdomain to define could be parametric, e.g. for a base-2 encoding of a number.
The central building block is a positive, divisible-by-10 integer (equivalently, a natural number of digits for a base-10 number), e.g. 10000 --> 4. This would have type something like
type UpperBound <: Singleton & PositiveInt, and then the values passed for representation would have type something liken: Int :| Greater[0] & Less[UpperBound]. This would facilitate, then, typesafe encoding of integers for things like field of view, timepoint, and imaging channel, with the number of characters encoding the number equal to the number of base-10 digits needed to encode the subdomain's max value (e.g. 4 for 9999 < 10000).As an even further generalisation, the base of the upper bound of the subdomain to define could be parametric, e.g. for a base-2 encoding of a number.