Well, if the requirement is to stay in the type, you could extend the type to include the point at infinity. That satisfies both programmer and the mathematician.

https://en.wikipedia.org/wiki/Projectively_extended_real_lin...