Hacker News Reader

I'm not very familiar with Python type checkers, so what follows may be completely off base.

> The reason is because an exception is a runtime check. It caught an error that is hidden until runtime. The better way is to encode this logic into a static type checking system so this error isn't even permitted to run

But in

  def div(x: Int, y: Int) -> Optional[Int]:
      return x // y if y != 0 else None

don't you have a runtime check? It has to do a runtime check of the value of y in order to decide whether or not to return None?

I don't see how this is encoding the logic of dealing with divide by zero into the type system or permitting the error to run. I'd expect that to deal with it in the type system to not prevent it at runtime would require y to be a type that does not allow 0 (does Python's type annotations allow constrained integers?).

Handling it by returning None means the caller has to deal with None. If it deals with it by just return None too, then its caller needs to deal with it do. If whatever code finally really deals with it instead of just passing it upwards is farther up than div's caller or maybe div's caller's caller it seems like what you've ended up with is something that is less clear than exceptions and requires more runtime work.

For those cases where the return None approach is better than using an exception, can you get rid of the runtime check for y being non-zero with something like

  def div(x: Int, y: Int) -> Optional[Int]:
      try:
          return x // y
      except ZeroDivisionError:
          return None

or do exceptions in Python occur sufficient overhead when not taken to make explicitly checking y win?

Python, historically, has not had zero-overhead exceptions. There is a runtime cost associated with a try block. 3.11 will be adding zero-overhead exceptions, though, per https://bugs.python.org/issue40222.

It encodes it into the type system at the function signature level. Optional[Int] is an Int with a None, so if you pass this type into f(x: Int) you get a type error because f(x: Int) is a function that deals with Ints, not Optional[Int]. So you get a degree of safety here.

As I mentioned this safety does not usually extend to the function definition. I stated that it can though (and it is in haskell and rust), and this is usually done through a feature called pattern matching. Pattern matching is available in python 3.10 but I'm not sure whether exhaustive type checking on pattern matching by external type checkers is available yet.

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.

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?

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.

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.

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.

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.

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.

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

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

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

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

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

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

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

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.

> First, Why does this even matter?

The reason you can't write my version using yours is that the types are less precise and you can't recover the imprecision in the output type after the fact. The only safe way to obtain an Int from an Optional[Int] is by providing a default value which doesn't exist in this case.

> The Optional[Int] doesn't exist so how do you create it?? You CAST

By casting I mean an unchecked narrowing conversion e.g. of the type Optional[Int] -> Int. There's no casting in my version.

> if you want to talk about "Well Established" then Optional is more well established

This is a false dichotomy, contracts are still used in static languages where you can't or don't want to try represent properties at the type level. You could for example define a function

    lookup: Map -> Key -> Optional[Value]

and still add preconditions that the map and key were non-null. The failure to uphold these represent a different kind of 'failure' than the key not being found so it wouldn't make sense to lift them into the return type.

> The safe version suffers from your same problem just moved

It didn't 'just' move, it moved to the point in the program you actually need to deal with the possibility of a zero divisor i.e. before calling div. Where does the divisor come from in the first place? You seem to be assuming there is necessarily some call to NonZero.fromInt at each call site to div but this is wrong. The non-zeroness of the divisor could be established at some prior point in the program and used in multiple places. In contrast your version has to deal with the possibility of returning None everwhere even if you've already established the property of the divisor beforehand.

>The reason you can't write my version using yours is that the types are less precise and you can't recover the imprecision in the output type after the fact.

Irrelevant to my statement. I said why does it even matter not why can't you do it. The answers are it doesn't matter at all AND you can't do it for EITHER case.

>The only safe way to obtain an Int from an Optional[Int] is by providing a default value which doesn't exist in this case.

No the safe way is through exhaustive type checking via pattern matching. If you're not sure what this is, look it up. Suffice to say it's static safety on all sum types including Optionals prior to execution.

>By casting I mean an unchecked narrowing conversion e.g. of the type Optional[Int] -> Int. There's no casting in my version.

There is 100% casting in your version. 100% percent. There is no narrow conversion here you're just making that shit up. The inverse of what you wrote is THIS:

       def convertDiv(f: (Int, NonZero[Int]) -> Int ): (Int, Int) -> Optional[Int]:

There is no way to create an Optional[Int] WITHOUT a typecast. I'm sorry, but your statement is definitively wrong no need to build some scaffold of strange logic around it and "narrow" the definition of a cast. I get your point though (even though I disagree). However, this does not change the fact that your example is completely wrong from a logical standpoint and completely off base.

>and still add preconditions that the map and key were non-null. The failure to uphold these represent a different kind of 'failure' than the key not being found so it wouldn't make sense to lift them into the return type.

Uh no. You can do Exactly what you did with NonZero[Int] with Key in your example. Imagine a map with RGB colors as keys.

   type KEY = Red | Green | Blue
   type VALUE = ...
   lookup: Map[KEY, VALUE] -> KEY -> VALUE

Like I said it's just your preference here. There is a false dichotomy when it comes to things being more correct when "Well Established" and that false dichotomy isn't coming from me. It's coming from you.

>It didn't 'just' move, it moved to the point in the program you actually need to deal with the possibility of a zero divisor i.e. before calling div. Where does the divisor come from in the first place? You seem to be assuming there is necessarily some call to NonZero.fromInt at each call site to div but this is wrong.

Ok let me reframe this. I completely AM not Assuming NonZero.fromInt at the call point AT all. Once you realize that your assumption is wrong, maybe you should consider the fact that you're NOT understanding me.

>The non-zeroness of the divisor could be established at some prior point in the program and used in multiple places.

The above is 100% what I am assuming. This prior point involves the creation of the type NonZero[Int] which involves: NonZero.fromInt. Every other mathematical operation (+,-,x^y,/,) returns an Int not a NonZero[Int] so this cast must occur. And that is my point. Think about it.

> In contrast your version has to deal with the possibility of returning None everwhere even if you've already established the property of the divisor beforehand.

This is where you're getting hung up. Let's clarify something your NonZero.fromInt is of the type:

   Int -> Optional[NonZero[Int]]

With that out of the way let us continue:

Yeah so my division returns an Optional which could be a None. I can either handle the None immediately or let it propagate all the way to IO and handle it just before it hits this wall. This is a bad thing I get it.

But your NonZero.fromInt Also returns an Optional which could be None. I can either handle the None immediately or let it propagate all the way to IO and handle it just before it hits this wall. This is a bad thing I get it.

Notice how the above two sentences are the same? That is what I mean when I say you're just moving the problem to another place but the problem essentially remains the SAME THING.

As I stated before and I'll repeat it again. The only reason why you prefer NonZero[Int] over Optional[Int] is the same reason why someone would prefer blue over red. There is no logic, rhyme or reason behind it. It is just your style and your personal taste.

> I said why does it even matter not why can't you do it

I've explained why it matters - the types are more precise in my version and if you start from that you can always throw away the extra precision if desired to get to your version. You can't go in the other direction, so starting from your version makes it impossible to safely recover an Int from the returned type of Optional[Int], even if you've already established the precondtion beforehand.

> There is 100% casting in your version

Creating an Optional[Int] from an Int is a conversion, not a cast. I thought it was obvious from the context but for the avoidance of any doubt, by 'casting' I mean an unsafe narrowing conversion. Optional[Int] is a larger type than Int, so it's trivial to create one from an Int:

    def pure(x: Int): Optional[Int] = Just(x)

you clearly can't safely go in the other direction, whether using pattern matching or otherwise. If you disagree, just complete the following definition:

    def fromOptional(o: Optional[Int]): Int =
        match o with
        | Some(i) => i
        | Nothing => ...

eventually you need to provide a default value for the case of no value.

> Imagine a map with RGB colors as keys.

Your example doesn't make sense, what would you expect (lookup Map.empty Red) to return? The optional return value is used to represent the key being missing in the map. Nonetheless the point I was making is that you wouldn't return Nothing from such a function in the event of a precondition failure e.g.

    def lookup(m: Map[K, V], v: K): Optional[V] =
        if m is None return Nothing
        ...

you would instead throw an exception if the input map is null and force the caller to handle it. The majority of static type systems are not powerful enough to encode arbitrary properties about values, so you have to decide which ones to check dynamically and which statically. Checking preconditions dynamically is reasonable if encodng them in the type system is too cumbersome.

> This prior point involves the creation of the type NonZero[Int] which involves: NonZero.fromInt

No, this is not necessarily the only way to create instances of NonZero. You could have a PosNat subtype with members one: PosNat and succ: PosNat -> PosNat. You could have a non-empty list type with a length member.

> Every other mathematical operation (+,-,x^y,/,) returns an Int not a NonZero[Int]

They don't return Optional[Int] either so I don't see how this is relevant. There's no reason the input has to come from some application of a different operator, it could come from configuration, user input, a property from some other type etc. The question is whether and how to model the constraints in the type. The constraint exists in the argument so it makes sense to constrain the input type, not widen the output.

> Notice how the above two sentences are the same?

Yes, if all you want to do is avoid establishing the property you care about and silently propagate some information-free 'failure' value to the top level, then you can do it either way. But the entire point of encoding properties in the types is to force you to establish them. These statements highlight the difference:

1. I've established the divisor is non-zero, called myDiv, received an Int and continue

2. I've established the divisor is non-zero, discarded that information to call yourDiv, recieved an Optional[Int] which cannot be empty, but which must be propagated. You could immediately unwrap the value but now you're just re-creating the dynamic behaviour of a function (Int, Int) -> Int which you've already rejected.

>Creating an Optional[Int] from an Int is a conversion, not a cast.

Ok man, take a look at this: https://en.wikipedia.org/wiki/Type_conversion

There is no garbage redefining of a well known word to fit your convenient argument. We are using English and well known terms. This is not obvious to anyone.

Let me illustrate what happened. YOu used a well known term INCORRECTLY, then redefined later claiming that your redefinition was obvious. That is a comedy excuse. No.

You were using a term incorrectly. You man handled the term and you are wrong in that regard.

> eventually you need to provide a default value for the case of no value.

So? It's still type safe. My point is you can't get rid of this problem at all, not even with NonZero int. But via an optional type you guarantee that it's handled. The Rest of your composition needs to live in the Context of that optional. This problem isn't solved by moving it to a post condition.

>Your example doesn't make sense, what would you expect (lookup Map.empty Red) to return?

Ok this I admit I'm wrong. I wasn't thinking detailed enough in that respect so my example was wrong . But this doesn't prove your case at all. There is nothing wrong with using a Maybe monad here. There is zero reason why you need to throw an exception.

>No, this is not necessarily the only way to create instances of NonZero. You could have a PosNat subtype with members one: PosNat and succ: PosNat -> PosNat. You could have a non-empty list type with a length member.

This level of pedantism is too extreme. Nobody uses that type of arithmetic. But if you want to go there fine. You now have a hole in subtraction as 3 - 3 would be a singularity. Your program can no longer use subtraction or addition.

Division and all other mathematical operations have incompatible types. Type casting is 100% necessary to use all operations. The only way I see your Peanno NonZero safetly working is to restrict division to be the exact First set of operations. Then a safe cast can be done without an optional from NonZero to Int for subsequent operations. This is the expansive type casting that is safe and what you're referring to earlier. Either way such an ordering restriction is highly unreasonable but it does offer total safety at the type level.

>They don't return Optional[Int] either so I don't see how this is relevant. There's no reason the input has to come from some application of a different operator, it could come from configuration, user input, a property from some other type etc. The question is whether and how to model the constraints in the type. The constraint exists in the argument so it makes sense to constrain the input type, not widen the output.

If it comes from user input are you saying there's a terminal where the user can never input a zero? If it comes from IO anything goes, you have to be prepared for Anything. Usually the input is String and String -> Int has a shitload of holes.

>Yes, if all you want to do is avoid establishing the property you care about and silently propagate some information-free 'failure' value to the top level, then you can do it either way. But the entire point of encoding properties in the types is to force you to establish them. These statements highlight the difference:

>1. I've established the divisor is non-zero, called myDiv, received an Int and continue

Number 1 cannot be established without creating a singularity or creating strange restrictions as I explained above. If all your program ever does is do division without accepting terms from IO then fine, you win, but let's be real. This is not a realistic expectation and that is my point.

Sorry for the confusion, but regardless of whether you call it casting, conversion, or something else, it's still trivial to do safely in one directly and impossible to do safely in the other. Given your fixation on the terminology I assume you've now accepted this.

> But via an optional type you guarantee that it's handled

It's not 'handled', which is the point. There's no default value so you have no option but to propagate the missing value. Callers that establish the precondition still have to deal with an Optional value even though it can't be empty. Callers which establish the precondtion through the types receive a more precise type and don't have this problem. Callers that establish the precondition in the more simply-typed version (Int, Int) -> Int also receive an Int. Only your version imposes the imprecision on the return type.

> There is nothing wrong with using a Maybe monad here. There is zero reason why you need to throw an exception.

The Optional[Value] returned from a map lookup is used to incidicate the possibility of a missing key, which is an expected outcome of the operation itself. Passing a null map represents a structural error in the construction of the program at the point the call is made. If you represent both in the same type you can't distinguish these two cases.

> You now have a hole in subtraction as 3 - 3 would be a singularity.

There's no hole here, subtraction on NonZero just has to return Int instead.

> If it comes from IO anything goes, you have to be prepared for Anything

Yes, if it comes from user input you have to establish the property dynamically. Encoding the property in the argument type forces you to actually do it (whether statically or dynamically), and help you push the constraint to the highest level. Putting the optionality in the return type doesn't force you do do this, and imposes a cost on every call that actually does.

>Given your fixation on the terminology I assume you've now accepted this.

I would call it fixation if it was some obscure reference. But it's not. You're calling a cat a dog. Literally everyone knows what type casting is. I'm saying hey buddy I know what you're talking about, but a cat IS NOT a dog.

I've always accepted the intent of what you're saying. You're just not understanding my intent. You literally didn't even address division coming before all other mathematical operations. I don't think you understood.

>It's not 'handled', which is the point.

It is handled. Otherwise it won't compile.

>There's no default value so you have no option but to propagate the missing value.

Understood. Let me put it this way an "=" represents a section of a program with no Optionals a "-" represents a section of a program with Optionals and an F represents a section of a program with a function that does division. A program is can be represented by a serial list of these characters. To you a program is bad if it looks like this:

-------------------F====================

After the division call the output is polluted with optionals because F returns an optional. You think this is bad.

You think a program should look like this:

-------------------F---------------------

And you think this is achievable with division if you use a NonZero Int type.

What I am saying is that it is not generally possible. To create a NonZero type your program will be polluted before the function call simply because Int->Optional[NonZero[Int]]:

===================F----------------------

>There's no hole here, subtraction on NonZero just has to return Int instead.

First of all this a type cast. subtraction and addition are defined on sets, not between two different sets.

Second off this defeats your whole point. You wanted to create a NonZero int for safety subtraction just made it unsafe again.

Third off does it return an int for 3 -3 and a nonzero for 4 - 2? So your subtraction returns a variant type. That basically opens up the same singularity as your null once you try to evaluate this sum type via pattern matching.

Wasn't your point this:

   f(x: NonZero, y: NonZero) -> int

If I do a subtraction operation BEFORE this function you can't even use the resulting zero value. So basically I have to turn subtraction into this which is identical from a cardinality stand point to returning a variant of a Int or NonZero:

   minus(x: NonZero, y: NonZero) -> Optional[NonZero]

> Encoding the property in the argument type forces you to actually do it (whether statically or dynamically), and help you push the constraint to the highest level.

As I said above nothing is pushed to a higher level you're just moving the singularity around. Making it happen at the type cast rather then the division.

>and imposes a cost on every call that actually does.

You either pay the cost before division or after. Pick your poison, that is what I am saying.

The only way your methodology works is if Division is the first thing that happens. Then your program looks like this:

F--------------------------------------

That's the only time a nonzero type makes better sense then a function that returns an optional.

Haskell throws an exception and rust panics on division by zero for ints.

This is just defensive programming.

The None state here is already an invalid state. If you want to use the type system to ensure correctness you would change the second argument to be a type representing multiplicatively invertible integers.

You need to employ pattern matching for exhaustive type checking to be deployed.

For haskell it will give you a warning. For Rust it will actually not compile. The key here is that you MUST use pattern matching.

If the compiler can figure out that you are dividing by zero at compile time then you will get those results. That is not a realistic expectation in general.

Having to wrap every division call in a maybe monad or rust result enum is bad from a usability standpoint and potentially unacceptable from a performance standpoint.

Exhaustive pattern matching is great. But not a replacement for other types of error handling.

Performance is a trade off and usability is arguable. There are ML style languages where a Maybe monadic value is the default return value of division due to the division by zero issue.

There are languages that employ this philosophy everywhere. Such languages are actually incapable of having a runtime error outside of edge cases like ffi.

Just so you know, you don't have to wrap every type in an enum. Types and enums share a bijective relationship. A type IS an enum and vice versa. You CAN in fact define an Int in terms of an enum (and an enum in terms of an int, in C). The mechanisms behind an Int and a bool are roughly the same, it's just the cardinality and mappings that are different. Pattern matching implementations usually check types based off of cardinality and do not differentiate between enums and other built in types like floats or ints.

This is probably all correct, but man... this just isn't fun at all. This isn't why I got into programming.

I'm sorry you don't find programming fun. I find it fun. And if you don't like this stuff, maybe it's the wrong career choice for you.