4 ms·

> The structure of the code handling this type of div is identical to code handling an actual exception You would never write an exception handler to handle su

> The structure of the code handling this type of div is identical to code handling an actual exception You would never write an exception handler to handle such a failure from div. The divisor being non-zero is a precondition of calling div in the first place, which is something the caller is responsible for upholding. You shouldn't ever need to write an exception handler to catch precondition violations. Do you also write handlers to 'handle' null dereferences? Representing the partiality in the return type is just pushing the responsibility to some code that can't reasonably do anything. > What then happens when I pass a zero? I've already explained this, you obtain a NonZero[Int] from a function fromInt : Int -> Optional[NonZero[Int]] and you can optionally add an unsafe version with type Int -> NonZero[Int] > All you did is propagate the issue to somewhere else Yes, the check has to be done somewhere since that is the point of encoding the property in the types. But encoding it in the argument type ensures the check is done before div is called which is where it needs to be done.

deltaonefour 5y ago
>You would never write an exception handler to handle such a failure from div. The divisor being non-zero is a precondition of calling div in the first place, which is something the caller is responsible for upholding. You shouldn't ever need to write an exception handler to catch precondition violations. Do you also write handlers to 'handle' null dereferences? Representing the partiality in the return type is just pushing the responsibility to some code that can't reasonably do anything. This is just your arbitrary preference. There is nothing wrong with going from either perspective. But your exception is completely worse from every quantifiable metric except for your opinionated qualitative metric. fromInt : Int -> Optional[NonZero[Int]] This is functions suffers from the same problem you describe. You're just trying to justify a convention of doing this check before rather than later. Also Your unsafe version is again worse because it will trigger an exception on zero, so I don't see how it helps your argument. >But encoding it in the argument type ensures the check is done before div is called which is where it needs to be done. This is the core of your argument and it is highly flawed. There is no "need" for it to be done this way. It is simply your preferred convention. Your argument loses on both fronts. Exceptions are definitively worse and Encoding non zero type safety into the parameter is not necessarily proven to be better.
- lkitching 5y ago
  > This is just your arbitrary preference It's not arbitrary since it's possible to write your function using mine but not vice versa. If you disagree then please implementing the following function without casting: def convertDiv(f: (Int, Int) -> Optional[Int]): (Int, NonZero[Int]) -> Int > You're just trying to justify a convention of doing this check before rather than later The convention that callers are responsible for upholding the preconditions of the functions they call is well established: https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract. You obviously can't fix precondition violations by checking the result after the fact. > Also Your unsafe version is again worse because it will trigger an exception on zero That is the point of the unsafe version, yes. Sometimes you will statically know the argument is non-zero e.g. NonZero(3). If you want to avoid an exception then use the safe version.
  - deltaonefour 5y ago
    >It's not arbitrary since it's possible to write your function using mine but not vice versa. If you disagree then please implementing the following function without casting: First, Why does this even matter? It doesn't. Being able to write something in terms of the other doesn't mean anything. Second you can't implement the converse without casting EITHER. The Optional[Int] doesn't exist so how do you create it?? You CAST. It's a zero cost implicit type in python and in C++. >The convention that callers are responsible for upholding the preconditions of the functions they call is well established: https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract. Should I use the fact that Optional is more well established then NonZero to win this argument? Yeah if you want to talk about "Well Established" then Optional is more well established then NonZero or this Design by contract convention that is so unestablished I barely even heard of it. Additionally even reading about this convention I see no requirement that division by zero must never return an undefined or that zero should never be the divisor. The description reads that these pre/post conditions just need to exist, but they're your choice what you need them to be. These conditions are encoded in the type. >If you want to avoid an exception then use the safe version. The safe version suffers from your same problem just moved. Nothing is magically solved by this move other than it fulfilling your arbitrary opinion and convention.

deltaonefour 5y ago

>You would never write an exception handler to handle such a failure from div. The divisor being non-zero is a precondition of calling div in the first place, which is something the caller is responsible for upholding. You shouldn't ever need to write an exception handler to catch precondition violations. Do you also write handlers to 'handle' null dereferences? Representing the partiality in the return type is just pushing the responsibility to some code that can't reasonably do anything. This is just your arbitrary preference. There is nothing wrong with going from either perspective. But your exception is completely worse from every quantifiable metric except for your opinionated qualitative metric. fromInt : Int -> Optional[NonZero[Int]] This is functions suffers from the same problem you describe. You're just trying to justify a convention of doing this check before rather than later. Also Your unsafe version is again worse because it will trigger an exception on zero, so I don't see how it helps your argument. >But encoding it in the argument type ensures the check is done before div is called which is where it needs to be done. This is the core of your argument and it is highly flawed. There is no "need" for it to be done this way. It is simply your preferred convention. Your argument loses on both fronts. Exceptions are definitively worse and Encoding non zero type safety into the parameter is not necessarily proven to be better.

lkitching 5y ago
> This is just your arbitrary preference It's not arbitrary since it's possible to write your function using mine but not vice versa. If you disagree then please implementing the following function without casting: def convertDiv(f: (Int, Int) -> Optional[Int]): (Int, NonZero[Int]) -> Int > You're just trying to justify a convention of doing this check before rather than later The convention that callers are responsible for upholding the preconditions of the functions they call is well established: https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract. You obviously can't fix precondition violations by checking the result after the fact. > Also Your unsafe version is again worse because it will trigger an exception on zero That is the point of the unsafe version, yes. Sometimes you will statically know the argument is non-zero e.g. NonZero(3). If you want to avoid an exception then use the safe version.
- deltaonefour 5y ago
  >It's not arbitrary since it's possible to write your function using mine but not vice versa. If you disagree then please implementing the following function without casting: First, Why does this even matter? It doesn't. Being able to write something in terms of the other doesn't mean anything. Second you can't implement the converse without casting EITHER. The Optional[Int] doesn't exist so how do you create it?? You CAST. It's a zero cost implicit type in python and in C++. >The convention that callers are responsible for upholding the preconditions of the functions they call is well established: https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract. Should I use the fact that Optional is more well established then NonZero to win this argument? Yeah if you want to talk about "Well Established" then Optional is more well established then NonZero or this Design by contract convention that is so unestablished I barely even heard of it. Additionally even reading about this convention I see no requirement that division by zero must never return an undefined or that zero should never be the divisor. The description reads that these pre/post conditions just need to exist, but they're your choice what you need them to be. These conditions are encoded in the type. >If you want to avoid an exception then use the safe version. The safe version suffers from your same problem just moved. Nothing is magically solved by this move other than it fulfilling your arbitrary opinion and convention.