This question already has an answer here:
- Should we define types for everything? 10 answers
It is common in strong, static typing to use different types even for variables with simple, primitive types to ease static analysis and indicate intent to the programmer. A color and a point in 3D space might both be represented by an array of 3 floats, but given different type names. In C, a lot of common types are simply typedef'd ints.
I'm wondering: just how far is it practical to take this? If you're writing a function that takes a float between 0 and 1 (perhaps it represents a probability distribution) do you create a separate type? What about a function that must take a non-zero integer? Would it be reasonable to create a type nonZeroInt, not for the purposes of encapsulation, but simply for type-safety?
You can take this arbitrarily far, encoding all preconditions of functions into the type system. For example, you could define a "primeNumber" type for the input to a function that only takes a prime. A function which must take two integers with no common factors could be changed to take one argument of type "coprimePair."
The two hypothetical functions above would presumably be part of a library that includes functions to generate prime numbers and coprime pairs, and return them with the appropriate type. If I wanted to call a function in that library that requires a prime number, and I didn't get it from the included prime-generating function, I'd have to explicitly cast an int, essentially forcing me do a reality check and ask myself, "Am I certain that this variable will always be prime?"
My specific question is this: How far is this philosophy ever successfully taken in practice? Are there programming languages, or well-respected programming texts, that encourage a philosophy that says: every function that cannot accommodate the entire range of any existing type as its input, and return a meaningful result for all possible inputs, should instead define a new type?