| On the other hand, here's a problem. Extend your numeric type tower to handle whatever new numeric types I come up with in an internally consistent manner. In haskell I have number types for things that automatically compute derivatives. I have number types for functions that go to number types so all vector spaces work like numbers as well. I have number types for arbitrary precision floating point numbers, and I can build these things on top of each other. It is a trade-off. We give up a bit of one thing to get something else. You can take either side of the deal. I'd argue that the weight of benefit is on the side where we don't have a magic type tower to reason about, but it is a perfectly reasonable stance to say that the thing you want is more important to you. On the other hand, I can turn around and argue that if what I really want is an ad hoc tower of numeric types I can just make a type for that and work inside it. data Number = Int Int | Rational Rational | Double Double | Complex (Complex Double) | ... instance Num Number Now I can opt into your model. Can you opt into mine? |
However, it's not the case that `data Number = ...` gets you everything. In particular, it gives up on the types! :)
For example, in Typed Racket:
-> (: norm : Real Real -> Real)
-> (define (norm x y) (sqrt (+ (sqr x) (sqr y))))
-> (norm -3 12)
- : Real
12.36931687685298
We've proved that the `norm` function always produces `Real` answers, even though `sqrt` might produce complex numbers given negative inputs. The sum type you've given won't let you prove that.