On Sat, Aug 8, 2020 at 16:41 Dominik Vilsmeier <dominik.vilsme...@gmx.de>
wrote:

> On 08.08.20 05:48, David Mertz wrote:
>
> On Fri, Aug 7, 2020, 6:03 PM Paul Moore <p.f.mo...@gmail.com> wrote:
>
>> > x: int[0:]  # any ints greater than or equal to zero would match,
>> others would fail
>> > x: int[:101]  # any ints less than 101 match
>> > x: int[0:101:2]  # even less than 101
>>
>> I suspect the biggest issue with this is that it's likely to be
>> extremely hard (given the dynamic nature of Python) to check such type
>> assertions statically.
>
>
> Yes, it's hard in the sense that it would require solving the halting
> problem.
>
> How is it any more difficult than already existing type checks? The
> proposal talks about type hints for static type analysis and hence implies
> using literals for the slices. There's no dynamic nature to it. You can
> define `int[x]` to be a subtype of `int[y]` if the numbers defined by `x`
> are a subset of those defined by `y`.
>
> Referring to one of the examples including `random.randint`:
>
>     def foo(x: int[0:11]):
>         pass
>
>     foo(random.randint(0, 10))
>
> Regarding static type analysis, the only information about
> `random.randint` is that it returns an `int` and hence this should be an
> error. If you want to use it that way, you'd have to manually cast the
> value:
>
>     foo(typing.cast(int[0:11], random.randint(0, 10)))
>
> This of course raises questions about the usefulness of the feature.
>
> By the way, I would find it more intuitive if the `stop` boundary was
> included in the interval, i.e. `int[0:10]` means all the integer numbers
> from 0 to 10 (including 10). I don't think that conflicts with the current
> notion of slices since they always indicate a position in the sequence, not
> the values directly (then `int[0:10]` would mean "the first 10 integer
> numbers", but where do they even start?).
>

> This of course raises questions about the usefulness of the feature.

I feel like this discussion boils down to one argument being the checking
is doable as long as you keep it to something with very limited usefulness
(static literal ranges) and the other being in order to make it useful
you'd need dependent typing and a sophisticated theorem prover.

I think about dependent typing when I look at TypeVar and Literal, but for
it to work, you'd have to be able to do gnarly things like add and compare
two TypeVars according to the operations of their literal types, like in
this case

A = TypeVar('A', int)
B = TypeVar('B', int)

def randint(a: A, b: B) -> int[A:Literal[1]+B]:  # ?
    ...

And randint(1, 1_000_000_001)

means B = Literal[1_000_000_001]

but plusone's type int[1:1_000_000_000] requires B
< Literal[1_000_000_000], which fails.

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.

Are we just talking about the language features here, or does this list
include ideas for tooling like mypy?

- Mike Smith
_______________________________________________
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/5ZPXR5FAL24PMFKTZ5ZGZ67WXLT6HNHH/
Code of Conduct: http://python.org/psf/codeofconduct/

Reply via email to