Deceitful Contracts

Bard suggested the following implementation for a Divide function in C#.

public static double Divide(double num1, double num2)
{
    if (num2 == 0)
    {
        throw new DivideByZeroException("Division by zero!");
    }
    return num1 / num2;
}

It looks like a standard C#-style implementation, with exceptions galore. The unfortunate thing about it is that the type signature

\mathrm{Divide}: (\mathrm{double}, \mathrm{double}) \rightarrow \mathrm{double}

lies. It looks like passing two \mathrm{double} values to Divide would return a \mathrm{double}, but this is not true if the second double has value 0. i.e., thinking about this in terms of a Hoare triple¹, the precondition to get a \mathrm{double} from Divide is not (\mathrm{double}, \mathrm{double}), but (\mathrm{double}, \mathrm{double} \setminus \{0\})

Ideally, the type of the function’s second argument would be \mathrm{double} \setminus \{0\}, making it impossible to pass an invalid (undesirable) value. This may or may not be possible or straightforward, depending on the language. In Ada and dependently typed languages like Idris or Agda, this is certainly possible (something to explore at another time.)

A second best option is to again make the function total and its type true, but now, instead of restricting the input, we change the return type to include the failure case (divide-by-zero).

It is standard to do this in a statically typed functional language like F#. In the specific case of our Divide function, it’d look something like

let divide (a: double) (b: double) =
    match b with
    | 0.0 -> None
    | _   -> Some (a / b)

having type \mathrm{double}\rightarrow \mathrm{double} \rightarrow \mathrm{option\langle double\rangle}, where \mathrm{option\langle double\rangle} has a value None (in the case where b = 0) or Some double.

To sum up: Keep your functions honest. Make them total and their types true by

1. Restricting input values to those needed, and only those.
2. As second best, expand the output type to cover for permissive inputs.