[deltaonefour]

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

[lkitching]

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.

[deltaonefour]

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