8 ms·

> 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 dyna

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

deltaonefour 5y ago
>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. Like I said think in terms of isomorphisms. Exceptions also force the caller to handle the code. There is no difference here. None is isomorphic to a Null and an exception is isomorphic to a result type. If you want context. Do this: type Result[Int] = Int | Exception[String] def div(x: int, y: int) -> Result[Int]: return x // y if y != 0 else Exception("Division by zero on line ${line}") The structure of the code handling this type of div is identical to code handling an actual exception. The main difference is type safety. Exceptions compile with a possible runtime error, Result types do not. Additionally your NonZero[Int] is not fully type safe. You have to think about long reaching consequences and precursors. Here you aren't thinking about the precursor. What generates this NonZero[Int]? Usually at some point you have some type casting function of the form: Int -> NonZero[Int] What then happens when I pass a zero? All you did is propagate the issue to somewhere else. Math doesn't have the syntax to fully compose two functions with different codomains and domains. So strict math formalism is irrelevant here. You can switch some attributes to isomorphic concepts (like how mapping division by zero to an element in a set called "undefined" is equivalent to the operation actually being undefined) but in the end you have to invent something because math simply doesn't have any elegant formal syntax to cover this codomain and domain mismatch. Therefore strict adherence to the concept that a Int can never be inserted into a div function is unnecessarily pedantic. Literally every other mathematical operation covers all of Z in both domain and codmain except for division.
- lkitching 5y ago
  > 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.

deltaonefour 5y ago

>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. Like I said think in terms of isomorphisms. Exceptions also force the caller to handle the code. There is no difference here. None is isomorphic to a Null and an exception is isomorphic to a result type. If you want context. Do this: type Result[Int] = Int | Exception[String] def div(x: int, y: int) -> Result[Int]: return x // y if y != 0 else Exception("Division by zero on line ${line}") The structure of the code handling this type of div is identical to code handling an actual exception. The main difference is type safety. Exceptions compile with a possible runtime error, Result types do not. Additionally your NonZero[Int] is not fully type safe. You have to think about long reaching consequences and precursors. Here you aren't thinking about the precursor. What generates this NonZero[Int]? Usually at some point you have some type casting function of the form: Int -> NonZero[Int] What then happens when I pass a zero? All you did is propagate the issue to somewhere else. Math doesn't have the syntax to fully compose two functions with different codomains and domains. So strict math formalism is irrelevant here. You can switch some attributes to isomorphic concepts (like how mapping division by zero to an element in a set called "undefined" is equivalent to the operation actually being undefined) but in the end you have to invent something because math simply doesn't have any elegant formal syntax to cover this codomain and domain mismatch. Therefore strict adherence to the concept that a Int can never be inserted into a div function is unnecessarily pedantic. Literally every other mathematical operation covers all of Z in both domain and codmain except for division.

lkitching 5y ago
> 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.