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