On Sat, Aug 8, 2020 at 5:49 PM Michael Smith <mich...@smith-li.com> wrote:
> This kind of thing is so powerful, and I would love to see tooling capable
> of it in the python ecosystem. I believe folks who say it's very hard to
> implement correctly, but I don't know that that's a good reason not to make
> the proposed range syntax legal for some primitive types like int. Tools
> like mypy can choose not to handle int[A:B] until they are ready, or
> forever, but someone else can still work on it.
As Steven notes, there *are* some compilers in static languages that do a
limited amount of this. But the cases where it is *provable* that some
bounds are not exceeded are very limited, or take a great deal of work to
construct the proof. I don't feel like Mypy or similar tools are going to
stray quite there. And in those static languages, a great deal of the
time, they must give up and just insert assertions to raise exceptions if
the bounds are violated rather than *proving* the constraint.
I slightly regret using the randint() example because you and I can so very
easily recognize that `random.randint(0, 1_000_000_001)` MIGHT return a
result of a billion-and-one. That was just to have something short. But a
great many computations, even ones that mathematically HAVE bounds, are not
easy to demonstrate the bounds. Let me try again, still slightly
hand-wavey.
def final_number(seed: int):
"Something mathy with primes, modulo arithmetic, factorization, etc"
x = seed
while some_condition(x):
while other_condition(x):
if my_predicate(x):
x += 1
elif other_predicate(x):
x += 2
else:
x -= 1
def my_fun(i: int[1:1_000_000]):
pass
my_fun(final_number(42))
Depending on what the called functions do, this is the sort of thing where
number theorists might prove bounds. But the bounds might depend in weird,
chaotic ways on the seed. For some it will fly off to infinity or negative
infinity. For others it bounces around in a small cycle. For others it
bounces around for billions of times through the loop within small bounds
until flying off. It's really NOT that hard to write functions like that,
even without really realizing their oddness.
Yours, David...
P.S. Compilers can do shockingly clever things. LLVM has an optimization
that took me by surprise. I was playing around with it via Numba a few
years ago. Actually, for teaching material; my intention was just to say
"Look, this is way faster than plain Python." But here's the case I
stumbled on:
Folks all probably know the story of Gauss in elementary school in which
(at least in anecdote) the teacher assigned the students to add all the
integers from 1 to 100 so she could get some coffee or whatever. Gauss had
the solution in a couple seconds to her annoyance. Because sum(range(1,
N+1)) == (N*(N+1))/2 by some straightforward reasoning that most 10 year
olds don't see (and in the story, neither did the teacher).
Anyway, my silly example for my training students (i.e. working programmers
and scientists) was loop to 100, add latest, with and without Numba. Then
do it up to a billion. My intentions was "Numba is lots faster, but has a
minor JIT overhead" ... my discovery was that "LLVM figures out Gauss'
simplification and does it in constant time no matter the N. After that I
looked at the LLVM bytecode to see, "Yup, it does." The optimizer is
pretty smart about variations in writing the code in some slightly
different ways, but I don't know exactly what it would take to fool it into
missing the optimization.
I asked one of the LLVM developers how I could find out what optimizations
are there. Their answer was "Become a core developer and study the source
code of LLVM." Apparently the Gauss thing isn't actually documented anyway
outside the code. :-)
--
The dead increasingly dominate and strangle both the living and the
not-yet born. Vampiric capital and undead corporate persons abuse
the lives and control the thoughts of homo faber. Ideas, once born,
become abortifacients against new conceptions.
_______________________________________________
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/YZRSXAGZHD7XS7LKG6OIKFLUB5YQBRDZ/
Code of Conduct: http://python.org/psf/codeofconduct/
