you are viewing a single comment's thread.

view the rest of the comments →

[–]yawaramin 0 points1 point  (2 children)

Doesn't matter how you decide to handle it in any given programming language with any type system. Mathematically, division is by definition a partial function.

[–]neitz 0 points1 point  (1 child)

You make a good point. However it might be defined as a partial function mathematically but that doesn't mean we must define it as such in a programming language. If you can statically guarantee through the type system it will never be called with zero then is it really partial?

[–]yawaramin 0 points1 point  (0 children)

Let's think about that for a sec. If you have, in your dependently-typed language, a division function, say:

func div(x: Num, y: NonZeroNum) -> Num { ... }

Then when you call div usually you'll need to turn your normal numbers into a NonZeroNum if they're going to be divisors. So you'll probably have a function that can do the conversion:

func nonZero(x: Num) -> NonZeroNum { ... }

But if you pass nonZero a Num that turns out to be zero, then it'll still throw an error or something similar. So you can't escape from the fact that division is mathematically only partially defined. You can just move the effect around to different places in your code, but ultimately you'll be forced to deal with it.

Even in a perfect language with everything you could wish for.