[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?