Constraining function inputs; what concept/terminology am I looking for?

Question

A function takes some set of inputs and creates a set of outputs; however there will be some set of invalid inputs. For example say we have F(a,b) => a / b and we constrain 'a' & 'b' to be numbers, and 'b' must never be zero.

The process of defining those constraints; what CS concept/terminology am I looking for?*

I'd like to improve my codebase's quality and I feel unexpected/unanticipated inputs are a big problem. I am looking for languages/frameworks** that it easier for developers to define those constraints; so I feel if I know the concept/terminology, I might have better success in my search.***

---

*Mathematically, I think I'm talking about domain. But is there a more specific CS term?

**Type constraints such as 'number' is standard for strongly typed languages, but having compile time constraint that say 'b' != 0 seems more esoteric. Runtime checks can be done, but I'd like to have something that defines the constraint on the interface/signature. Something of a 'strongly set range/set' of inputs.

***While my goal is to find framework/language, product recommendations get marked as off topic on most stack exchange sites. So I'm looking for the underlying concept.

Answer 1

I believe the concept you are looking for, is simply a Type. For example, one possible type of the function F from your question would be: F :: (Number, NonZeroNumber) -> Number.

There are of course many other related concepts, such as Contracts. But they can mostly be interpreted as just different ways to write types. In fact, I believe there is actually a proof that (certain kinds of) contracts are always expressible as (potentially exponentially large) types.

As a very general rule, there are three different ways of turning a partial function into a total function:

• Modify the Range
• Modify the Domain
• Modify the Codomain

Let's look at division. Typically, we would define division like this:

(/) :: (Number, Number) -> Number
a / b = … naive implementation of division

Of course, this function is partial. It will diverge for b = 0.

We can fix that by modifying the Range:

a / 0 = 0
a / b = … naive implementation of division

Now, our function is total: it does not diverge if b = 0. It returns a result. It is a wrong result, of course, but it is not an error!

The second option, as already mentioned above, is to modify the Domain:

(/) :: (Number, NonZeroNumber) -> Number
a / b = … naive implementation of division

Problem solved. Now, it is impossible to pass in b = 0, and there can never be an error.

A third option is to modify the Codomain:

(/) :: (Number, Number) -> Option Number
a / 0 = None
a / b = Some (… naive implementation of division)

None of these require any fancy stuff. However, even if we were to introduce something like Contracts into our language:

(/) :: (Number, Number) -> Number 
    where
        b ≠ 0
    in
        a / b = … naive implementation of division

This can be viewed as equivalent to defining an unnamed type __someUnnamedType__ = Number \ { 0 } and rewriting the function definition to

(/) :: (Number, __someUnnamedType__) -> Number
a / b = … naive implementation of division

As I mentioned above, I vaguely remember reading about a proof that contracts and types have equivalent expressive power, but some contracts may generate exponentially large types. So, whether to choose contracts or types partially depends on usability and convenience.

The most well-known Contract system is probably Eiffel's, but I have a soft spot in my heart for Microsoft Research's Spec#.