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