On Sat, Aug 08, 2020 at 01:28:59AM -0400, David Mertz wrote:
> On Sat, Aug 8, 2020, 1:12 AM Steven D'Aprano
>
> > Static languages often check what
> > bounds they can at compile time, and optionally insert bound checking
> > runtime code for ambiguous places.
>
>
> Yep. That's an assert, or it's moral equivalent.
No, asserts are not checked at compile time. Assertions are purely
runtime checks. But bounds checking can be done (at least in part) at
compile time, depending on how smart your compiler is. (In the case of
Python, that would be entirely delegated to a third-party checker.)
If a static checker knows that x is a float, and that n is an int
between 0 and 100, it shouldn't be hard to tell that this is a bounds
error:
x: float
n: int[0:100]
n = int(x)
but this isn't:
n = int(x) % 5
But there is a big gap between what a human can reason about code and
what a tool can do in practice (as opposed to in theory), and I don't
know what the state of art in range checking is, or how sophisticated it
may be.
Compared to type systems, compile time range checking has been neglected
for decades and (as far as I can tell) the state of the art is far more
primitive. But I could be wrong and this could be one of the simplest
things that they can handle for all I know :-)
We should remember that the requirement for static checking isn't to
detect at compile time that something *will* be a runtime error, but
that it *could* be a runtime so that you can fix your code to avoid the
possibility. Just as type checking doesn't tell you that you certainly
will get a type error at runtime, only that you could.
I suggested this proposed feature be deferred unless people in the MyPy
and other static checking projects express interest. It may be that
nobody in the MyPy and other static checker projects has the knowledge,
time or interest in pursuing this, in which case supporting this would
be a waste of time.
> Here's a deterministic program using the hypothetical new feature.
>
> def plusone(i: int[1:1_000_000_000]):
> return i+1
>
> random.seed(42)
> for n in range(1_000_000):
> random.randint(1, 1_000_000_001)
>
> Is this program type safe? Tell me by static analysis of Mersenne Twister.
I assume there was supposed to be a call to plusone there :-)
randint will surely be declared as returning an int, since we can't be
more specific than that without getting into serious levels of
automated correctness checking.
Any checker capable of doing bounds checks would know that the range of
possible ints is unbounded in both directions, and therefore an int does
not fit into the range [1:10**9]. Hence that will be a static bounds
check failure: the checker detects that there is a chance that the input
to plusone could be out of range.
> Or if you want to special case the arguments to randint,
Of course not.
> will, lots of
> things. Let's say a "random" walk on the integer number line where each
> time through the loop increments or decrements some (deterministic but hard
> to calculate) amount. After N steps are we within certain bounds?
Let's be less vague:
def step()->int[-3:4]:
pass
n = 0: int[-100:101]
for i in range(N):
n += step()
You and I can reason that after N steps, the maximum possible value of n
is 3*N, which could be greater than 100 unless N was provably less than
34, which it may not be. And so the bounds check fails.
I know very little about the state of art of bounds checking, but I
would imagine that this would probably be beyond the capability of a
simple checker, and maybe a sophisticated one too, but not the most
sophisticated formal correctness proof checkers.
So what? The value of static checking is not diminished by the problems
not found, since they wouldn't be found if you had no static checking in
the first place. The value of static checking is in the problems which
are found.
Whether or not MyPy etc are capable of such range checking, or even
simpler checks, is a question best asked of them. If they have any
interest in range checking, adding subscripting to `int` would be easy.
Until then, YAGNI.
--
Steven
_______________________________________________
Python-ideas mailing list -- python-ideas@python.org
To unsubscribe send an email to python-ideas-le...@python.org
https://mail.python.org/mailman3/lists/python-ideas.python.org/
Message archived at
https://mail.python.org/archives/list/python-ideas@python.org/message/SR4SVS6MOWZY7NX5L4NBIFBWLNKZH7ZP/
Code of Conduct: http://python.org/psf/codeofconduct/
