[obastani]

This breaks down because it's not easy to statically reason about when a variable is a NonZeroNumber. For example, what is the type signature for subtraction of two NonZeroNumbers? You can't guarantee that it isn't zero, so it has to be a Number. Thus, you can't divide by the difference. You could use a more powerful type system to reason about these kinds of constraints, but then type checking quickly becomes undecidable (or at least very, very expensive).

[naasking]

> For example, what is the type signature for subtraction of two NonZeroNumbers? You can't guarantee that it isn't zero, so it has to be a Number.

You can encode this failure as well, so at least the possibility becomes explicit:

    NonZero -> NonZero -> Either NonZero Number

Oleg also showed you can make an even safer statically checked version with pretty standard type theory and modules:

https://okmij.org/ftp/Computation/lightweight-guarantees/lig...

[vidarh]

    a = b - c

    if a != 0 then x = y / a

Here you can infer that the type of 'a' inside the 'then' is a NonZeroNumber. "All" you need is for the type checker to be able to recognize when a conditional acts as a guard against a subset of the possible types.

[tromp]

But if we're dividing by (a-1) then recognizing that it's safe may require a type NonOneNumber. And in other cases perhaps NonFortyTwoNumber. Where does that end?

[vidarh]

Only in as much as it would require the type checker to be able to express and operate on expressions constraining or combining types, not name every one. E.g. being able to recognise that in this:

   if a < 2 then exit

.. afterward, "a" has a named numeric type fully covered by its previous type combined with the extra constraints of the check if that allows picking a more constrained type, and its real type is further constrained to the subset a>=2, and be able to reconcile that this means 'a' can't be 1.

In practice, yes, you can absolutely get into situations where this will mean you end up writing extra checks to prove to the compiler that a value can only be within the required subset if the type checker couldn't figure it out. How often will depend on how advanced your type checker is.