2.7.35 Types Tutorial Exercise 3

We can make ‘inf - inf’ be any real number we like, say, ‘a’, just by claiming that we added ‘a’ to the first infinity but not to the second. This is just as true for complex values of ‘a’, so nan can stand for a complex number. (And, similarly, uinf can stand for an infinity that points in any direction in the complex plane, such as ‘(0, 1) inf’).

In fact, we can multiply the first inf by two. Surely ‘2 inf - inf = inf’, but also ‘2 inf - inf = inf - inf = nan’. So nan can even stand for infinity. Obviously it’s just as easy to make it stand for minus infinity as for plus infinity.

The moral of this story is that “infinity” is a slippery fish indeed, and Calc tries to handle it by having a very simple model for infinities (only the direction counts, not the “size”); but Calc is careful to write nan any time this simple model is unable to tell what the true answer is.