@Hlaaftana yeah it makes sense that this was something that was just “good enough” at some point and could use better design.
> In my scripting language I've been trying to do something like this, where > refinement types are "properties" over concrete types … Very cool to see how you’re approaching this. The way I’m trying to do it in Nim is similar - a wrapper type with a predicate and some value(s). There can be an explicit constructor to check the predicate at runtime and an implicit converter to weaken or forget the predicate. @ElegantBeef Cool idea, but I don’t think it quite works. For instance, Naturals are closed under addition but not subtraction (indeed one way to define negative numbers is as equivalence classes of pairs of naturals). As for the default value of zero, I understand _why_ it’s the case, it’s just unfortunate. @demotomohiro Saying integers mod N is somewhat misleading too - subtraction and division are defined as per the integers, not the way you’d define them as residue classes. Naming things is hard. Also, yes, they are most suitable for parameters; it _is_ nice to be able to declare parameter preconditions in code.
