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

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.

• Even runtime tests dont suffice sometimes. However those cases are not practical by any means (for example, let $b$ represent a TM that halts on $a$). So O doubt you will easily find a theoretical CS term for this. It might actually better for you to directly ask at stack overflow since they are the experts in terms of frameworks and languages :) Sep 2, 2021 at 5:46
• Oh I like that TM halt example! And I see why you suggest asking SO; but it might get marked as off-topic as a product recommendation. So ignore the automatic part (I'll edit the question too). In the same way strong types help people manually set the right shape of inputs, is there a 'strong range/set' that can help people manually set the right set of inputs? Sep 2, 2021 at 12:12
• Is guard or precondition the word you are looking for? Sep 2, 2021 at 12:21
• Precondition looks pretty similar; I'll add that to my key word search! Sep 2, 2021 at 23:24

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#.