On Sat, Aug 8, 2020 at 5:49 PM Michael Smith <michael@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.