You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2. But I think, the latter representation should probably be prefered. With it, :+ always has a number as its left argument and a digit as its right. Without the () :+ we get ugly exceptional cases. You can see this, for example, in the instance declarations for Compare. With the second representation, we could reduce the number of instances dramatically. We would define a comparison of digits (verbose) and than a comparison of numbers based on the digit comparison (not verbose).
Even if () would be preferred from the programmers point of view (I'm not sure how much we could reduce the number of instances though), it makes the representation less attractive on the user-side. Anyone using the library would find it annoying and would wonder why is it neccessary.
I wouldn’t wonder. Leaving out the () :* part just works because our type-level “values” are not typed, i.e., there aren’t different kinds Digit and Number but only kind *. If :+ would be a data constructor (on the value level), it would take a number and a digit argument which would forbid using a digit as its left argument. So I consider using a digit on the left as “unclean”. It’s similar to using a number as the second part of a cons cell in LISP.
How 'bout treating :+ as similar to `append' rather than similar to `cons'? Basically treat :+ as taking 2 numbers (rather than a number and a digit). Stefan