[Spivak]

This ends up being a super unergonomic API in practice because you would need to modify the type-checker to infer positive integers correctly. Nobody wants to go through the effort of

    NonZero = NewType(‘NonZero’, int)

    if x != 0
        x = NonZero(x)

just to call your function, especially since you still have to handle the case where someone does NonZero(x) blindly without checking. Should the constructor throw?

[lkitching]

The check has to go somewhere and the caller to div has the most context in the event the divisor is 0. If you return an optional from div then you either impose the check on all the callers, or just propagate None everywhere and some top-level function has to deal with mysteriously missing values.

The NonZero type should be responsible for checking the wrapped value is non-zero, you will probably want safe and unsafe constructor functions

    Int -> Optional[NonZero[Int]]
    Int -> NonZero[Int]

where the unsafe version throws.

If this is overkill for your application then I'd prefer throwing an exception in div rather than encoding the failure in the return type.

[deltaonefour]

That's your preference. However from a safety standpoint it is better to return an Optional[Int] or pass a NonZero[Int]. These two checks eliminate an entire class of runtime errors from ever occurring and that is a quantitative metric that is definitive.

[lkitching]

My first preference is to change the type of the divisor to NonZero[Int], and throwing an exception within div is only my second preference. It doesn't make sense to change the return type of div to Optional[Int] because the success or failure or the operation is determined entirely by a property of one of the arguments, which the caller can always check. Making div partial and encoding it in the return type just moves the the problem away from the place it occured and can actually be handled.

[deltaonefour]

It does make sense because the next thing handles the return type must be equipped to handle the optional type or the program won't run/compile at all.

This still moves the check out of runtime and into a static check. An exception means the error is handled runtime and as I said before is a definitively worse metric.

Let me put it more simply. An exception means that you can compile an error or mistake and it might accidentally make it to production. This happens because exceptions are only thrown on compiled programs during runtime.

An optional means that run time errors of this nature are impossible to happen. A program that throws an exception on division by zero is impossible to even EXIST. This occurs because if the optional is used, the static type checker will prevent such a program from even compiling. That is why it is definitively better.

[lkitching]

Div always returns an int as long as the precondition - that the divisor is non-zero - is satisfied. The caller is always responsible for ensuring the precondition is satisfied which means the caller must ensure the divisor is non-zero before making the call. Checking it dynamically and throwing an exception does have the drawbacks you state, but if you're going to represent the contract in the type system then you do that by constraining the type of the divisor, not widening the return type.

Your encoding has really changed the meaning of the div function - it now always accepts any two arbitrary ints and always allows the possibility of returning None. So you've weakened both the precondition and the postcondition, which is now easier for the caller but imposes a cost on every location where the return value is used. As the optionality encoded in the value propagates further from the call to div, the context for the source of the missing value is lost. This is 'safer' in the sense of avoiding crashes at runtime but doesn't actually help resolve the actual issue of avoiding a zero divisor when calling div.

[deltaonefour]

>Your encoding has really changed the meaning of the div function - it now always accepts any two arbitrary ints and always allows the possibility of returning None.

No it did not. That is simply your interpretation of it. I can rename "None" to "undefined" or to "Exception" and the etymological meaning is now more inline with your thinking.

The concept of exception or undefined can be encoded into a type or the set of all ints. What you are doing is saying is roughly equivalent to, "No I want to use the mathematical definition of Z, and I don't want to encode the reality of what's actually going on into the type."

You are getting hung up on a wording issue because you are stuck on the mathematical concept of undefined and division of Ints. Think of the problem from a higher mathematical perspective of sets and define a set (aka type) that fits the use case. That's just one perspective on the flaw in your thinking. There is another isomorphic perspective as well:

There is nothing weak going on here. There is no difference in saying that division by zero maps to "undefined" vs. Not defining it period. The concepts are isomorphic. When you construct the mapping in the english language when you talk to people. You literally say "division by zero is undefined" or "division by one is the same number" all these sentences are equivalent to saying "division by x/y/zero/ maps to undefined/z/somenumber."

Don't get too lost in mathematical conventions. Understand the higher meaning behind the concepts and you'll be much more flexible.

>This is 'safer' in the sense of avoiding crashes at runtime but doesn't actually help resolve the actual issue of avoiding a zero divisor when calling div.

You're not seeing the bigger picture. The only way to avoid a zero divisor is to use your made up type NonZero[Int]. There's no other way. Not even your exception handling can prevent a zero divisor.

The best way to do this is to FORCE the user to handle a zero divisor pre-compile time. This does not happen with an exception. Your program just crashes.

The pattern matching I illustrated above is a mechanism for forcing the user to handle any zero divisor related logic or the program won't Compile period. It is definitively better.

Think of it this way. Exceptions are cheating. It's some sort of escape hatch built into the language. It's better to have no escape hatches. Build all possible outcomes into the type.