0
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ 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 :) $\endgroup$
    – nir shahar
    Sep 2, 2021 at 5:46
  • $\begingroup$ 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? $\endgroup$
    – user8187
    Sep 2, 2021 at 12:12
  • $\begingroup$ Is guard or precondition the word you are looking for? $\endgroup$
    – Janmar
    Sep 2, 2021 at 12:21
  • $\begingroup$ Precondition looks pretty similar; I'll add that to my key word search! $\endgroup$
    – user8187
    Sep 2, 2021 at 23:24

1 Answer 1

0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.