[lkitching]

For division you really should put the requirement for the non-zero check in the type of the divisor instead of propagating failure to the caller e.g.

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

Exceptions at least have the benefit of retaining the location the context for the error occurred which gets lost without extra bookeeping when using optionals.

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