Differences Between Mathematics and ML

Up till now, we have been looking at the similarities between math and ML. Now we look at the differences: ML typechecking only approximates the true (mathematical) type of a function.

Recursive function definition e.g., letrec f x = f x might have type . But we can have divergence/partiality: . Here, denotes nontermination. It differs from all the other values of which we speak: it cannot be tested for. It is undetectable. Any test for equality to would be an immediate solution to the halting problem, which we know to be unsolvable. ML types, i.e., , are an approximation to the true mathematical type. The halting problem is undecidable, so we cannot mechanically ``type-check'' this problem away.

Differences:

• Nonterminating programs do not define functions!
• ML uses exceptions for detectable errors, e.g., division by zero. These are system exceptions. But we also have ``mathematical'' exceptions, e.g., or . e.g. a ``safe'' division function has type