28 April 2023

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^{1}, 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
| (a / b) | _ -> Some
```

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

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

\{p\} f \{q\}: If the input x of f satisfies precondition p, then the output f x of f satisfies postcondition q.↩︎