[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.

[lkitching]

> There is nothing weak going on here

The type for your static version of div is:

    def div(x: Int, y: Int) -> Optional[Int]:

The precondition for the dynamic behaviour of div is that the divisor is non-zero. If you want to think of it in set terms this means y must be a member of Z - #{0}. But your encoding allows any member of Z. This is a larger set and therefore a weaker precondition.

Likewise the postcondition of the dynamic version is that an Int is returned, but yours only guarantees an Optional[Int]. Again in set terms this is something like Z + #{None} which is a larger set than Z and therefore a weakening of the post condtion.

Your version encodes the dynamic behaviour of throwing an exception in the return type, but I'm saying that

    def div(x: Int, y: NonZero[Int]) -> Int

is a more precise static definition of the behaviour of div, and if you're going to add types to the dynamic version you should prefer this approach. Our two definitions are not equivalent since your function can easily be implemented with mine:

    def yourDiv(x, y) = map (fun nz: myDiv x nz) (fromInt y)

but you can't (safely) implement my version using yours since it returns an Optional[Int] and an Int is required. This shouldn't be surprising since algebraically (Int, Int) -> Option Int is a larger type than (Int, NonZero[Int]) -> Int.

> You're not seeing the bigger picture. The only way to avoid a zero divisor is to use your made up type NonZero[Int]

Obviously I know this because I suggested using NonZero[Int] in the first place. Your version accepts an Int divisor and just encodes the partiality in the return type. But this doesn't force the user (i.e. caller) of div to handle a non-zero divisor at all, it forces the user of the return value to handle a potential missing value without any context for why it was missing. Propagaging this missing value isn't 'handling' the error at all, since that can only be resolved by ensuring the divisor is non-zero before calling div.