Does any programming language have a concept of checking the type and value of a given parameter without adding an explicit if (myParam < 0) { .. } within the function?

A pseudocode example:

function myFunction(int myParam >= 0) {
    return myParam + 2;

// myFunction(1)     would return 3
// myFunction(-1)    would raise an error
// myFunction("abc") would raise an error
// myFunction(2.1)   would raise an error
// myFunction()      would raise an error

or maybe:

function myFunction(int myParam 0) {
    return myParam + 2;
  • 1
    It's not part of the language(s), but .Net has Code Contracts: docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/… – MetaFight Jan 3 '18 at 12:42
  • Haskell and some other languages allow overloads with exact values. Ada has general purpose guard expressions for synchronization though I'm not sure if they work for function overloads. – Erik Eidt Jan 3 '18 at 15:47
  • 1
    My first thought here is, "That's just a type check, but you forgot to use the correct type." In other words, define a type that only allows the valid values and have your function take that type instead of the much broader int. Include an easy means of conversion, if necessary. In this specific case, many languages even already provide some sort of unsigned integer type. Potentially more interesting would be a type restricted by a runtime value, rather than a constant. – 8bittree Jan 3 '18 at 23:37

In dependently-typed languages, static types can depend on runtime values. This essentially means that you can encode any logical statement as a type. I am not familiar enough with dependent typing to show you what your example would look like, but essentially, it would be a compile time type error to pass a number less than zero.

Or, to put it more precisely: there needs to be a proof that any value you are going to pass is greater than zero. Who is responsible for how much of that proof, the programmer or the compiler, that is basically where different dependently-typed languages differ. Note that this generally also means that the language cannot be Turing-complete, because per the Curry-Howard Isomorphism, expressing non-termination (e.g. an endless loop) is equivalent to proving a false statement.

The standard example of what a dependently-typed language can do is to carry the size of a list as part of the list's type, i.e. you can create a type List<T, n>, where T is a Type Variable and n is a Value Variable, and the compiler is able to either infer or prove or check (depending on how you want to use it) that, e.g. you are only allowed to concatenate a List<A, b> and a List<A, c> (where the list elements have the same type, this is boring, any language with generics can do this) and that the return type is List<A, b+c> (this is the fascinating bit).

Another approach is Design-by-Contract. The idea of DbC in general is that types have invariants that must always be true and operations have preconditions that must be true when the operation starts and postconditions that must be true when the operation finishes. The reason why it is called "Design by Contract" is that there is a contract between the caller and the callee: the caller is responsible for ensuring that the preconditions are met, in turn the callee guarantees that it will meet the postconditions.

The prime example of a language which integrates DbC is Eiffel. However, in Eiffel, contracts are checked at runtime. (Note that contracts can be arbitrary predicates, and as such checking them at compile time is equivalent to solving the Halting Problem.) This is by far the most widespread way of implementing DbC, injecting runtime contract checks for the precondition at the beginning of the method and runtime contract checks for the postcondition and all invariants at the end of the method.

In Eiffel, your code would look roughly like this:

myFunction (myParam: INTEGER): INTEGER is
  myParam_is_nonnegative: myParam >= 0
  Result := myParam + 2

(The label for the precondition is optional but helps in debugging and logging.)

Microsoft Research went one step further and designed Spec♯, a superset of C♯ 2.0 with built-in contracts. The interesting thing about Spec♯ is that it uses a theorem prover and tries to prove (or find counterexamples for) the contracts at compile time. However, remember what I wrote above: this is equivalent to solving the Halting Problem, so it cannot possibly work reliably in the general case. In particular, there will usually be some contracts where the theorem prover can prove that they will never be violated, some for which the theorem prover can prove that they will always be violated, some for which it can show that they might be violated under certain conditions, and some for which it can't tell. Note that if there are some contracts which may be violated, the checker must still reject the program, otherwise it would be unsafe. In that case, you will have to rewrite your code so that the theorem prover does understand it, purely to circumvent restrictions of the theorem prover.

In Spec♯, your code would look roughly like this:

int myFunction(int myParam)
    requires myParam >= 0;
    return myParam + 2;

Later, Microsoft extracted the technology behind Spec♯ into a bytecode postprocessor which searches for "magic library calls" and transforms them into contract checks. This is particularly cool because it allows it to be used with any language without changing the language. However, it is also much less syntactically convenient:

using Microsoft.Diagnostic.CodeContracts;

int myFunction(int myParam)
    Contract.Requires(myParam >= 0);
    return myParam + 2;

For the specific problem in your question, but not the general case of validating parameters against arbitrary rules, you could use subrange types. Some languages allow you to specify a type that is a subrange of an ordinal type. Algol, Pascal and its successors (Modula-2, Oberon, Component Pascal), Ada, and Nim are some examples. In Pascal, your code would look roughly like this:

FUNCTION myFunction(myParam: 0..MAXINT): INTEGER;
   myFunction := myParam + 2

Of course, if we are going down this road, then your specific example can also be achieved using an unsigned integer type.

In languages that don't have any of this, you could use the Tiny Types Pattern, where you don't use general types such as int but instead wrap everything into "tiny" types that know how to validate themselves (example in Scala):

class NonNegativeInteger(n: Int) {
  require(n >= 0)

  def +[T](other: T)(implicit num: Numeric[T]) = num.plus(other, n)
  // and so on

def myFunction(myParam: NonNegativeInteger) = myParam + 2

myFunction(new NonNegativeInteger(1)) //=> 3
myFunction(new NonNegativeInteger(-1)) // *runtime* error
myFunction("abc") // *compiletime* error
myFunction(-1) // *compiletime* error
myFunction(1) // unortunately, also *compiletime* error

Note: here, require is not part of some DbC implementation, it is just a method defined in the standard library that throws an exception if its argument is false. And the body of the class is the constructor, so all this does is throw an exception in the constructor if you try to construct a NonNegativeInteger with a negative integer.

| improve this answer | |

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.