Supporting list lengths
Let's say I have the following function: ```python def spam(a: str, b: str, c: str, d: int = 42): ... ``` Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ``` That will execute fine and actually result in appropriate types for those arguments. Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass. Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'?
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time? I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)). On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/>
Are you asking for a higher-kinded (I believe?) `split` that can specify in its return type how many elements it returns? A problem with that is `some_str.split(a_delimiter, 2)` is only guaranteed to return an array of *up to* 3 (maxsplit+1) elements. (In fact, your example only works by accident -- it should be `split("a/b", 1)` to guarantee the call will always succeed.) -- Teddy On Mon, Sep 21, 2020 at 12:38 PM Guido van Rossum <guido@python.org> wrote:
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time?
I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)).
On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/> _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: tsudol@google.com
On Mon, Sep 21, 2020 at 1:23 PM Teddy Sudol <tsudol@google.com> wrote:
Are you asking for a higher-kinded (I believe?) `split` that can specify in its return type how many elements it returns? A problem with that is `some_str.split(a_delimiter, 2)` is only guaranteed to return an array of *up to* 3 (maxsplit+1) elements. (In fact, your example only works by accident -- it should be `split("a/b", 1)` to guarantee the call will always succeed.)
Yep, I basically screwed up by misremembering that the count argument to str.split() is a max count, not a guaranteed count. Sorry about the noise on this (although I guess the question somewhat can still be asked had I chosen to create a function that guarantees the length of a list).
-- Teddy
On Mon, Sep 21, 2020 at 12:38 PM Guido van Rossum <guido@python.org> wrote:
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time?
If str.split() worked the way my brain told me it worked, I would have asked if `str.split(self, sep: str, maxsplit: int = Literal[2]) -> SizedList[2, str]: ...` made sense. -Brett
I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)).
On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/> _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: tsudol@google.com
To be clear, my point was that the problem is a lot harder than it looks at first, not just saying your example was bad! Do other languages have something like SizedList? I can't recall any off the top of my head. -- Teddy On Tue, Sep 22, 2020 at 10:21 AM Brett Cannon <brett@python.org> wrote:
On Mon, Sep 21, 2020 at 1:23 PM Teddy Sudol <tsudol@google.com> wrote:
Are you asking for a higher-kinded (I believe?) `split` that can specify in its return type how many elements it returns? A problem with that is `some_str.split(a_delimiter, 2)` is only guaranteed to return an array of *up to* 3 (maxsplit+1) elements. (In fact, your example only works by accident -- it should be `split("a/b", 1)` to guarantee the call will always succeed.)
Yep, I basically screwed up by misremembering that the count argument to str.split() is a max count, not a guaranteed count. Sorry about the noise on this (although I guess the question somewhat can still be asked had I chosen to create a function that guarantees the length of a list).
-- Teddy
On Mon, Sep 21, 2020 at 12:38 PM Guido van Rossum <guido@python.org> wrote:
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time?
If str.split() worked the way my brain told me it worked, I would have asked if `str.split(self, sep: str, maxsplit: int = Literal[2]) -> SizedList[2, str]: ...` made sense.
-Brett
I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)).
On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/> _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: tsudol@google.com
SizedList list is not just a type, it is a dependent type (in a way that the actual type is dependent on the concrete value). That's something very few languages have. And using a language with dependent types is a nightmare for a regular developer. There are also two projects that can partially solve this problem (based on phantom types, which are just shallow / phantom wrappers for actual types): - https://github.com/antonagestam/phantom-types - https://pypi.org/project/phantoms/ (WIP in our dry-python family) They have a notation like `NonEmpty[List[int]]`, that guarantees that list has at least one element. And can be extended to use something like `Sized[List[int], 5]` which guarantees that list has specifically 5 elements. One more thing that might be helpful: monadic `NonEmptyList` type. I am not sure that there are any actual implementations in Python, but we are tracking this potential feature for dry-python/returns here: https://github.com/dry-python/returns/issues/257 вт, 22 сент. 2020 г. в 20:24, Teddy Sudol via Typing-sig < typing-sig@python.org>:
To be clear, my point was that the problem is a lot harder than it looks at first, not just saying your example was bad!
Do other languages have something like SizedList? I can't recall any off the top of my head.
-- Teddy
On Tue, Sep 22, 2020 at 10:21 AM Brett Cannon <brett@python.org> wrote:
On Mon, Sep 21, 2020 at 1:23 PM Teddy Sudol <tsudol@google.com> wrote:
Are you asking for a higher-kinded (I believe?) `split` that can specify in its return type how many elements it returns? A problem with that is `some_str.split(a_delimiter, 2)` is only guaranteed to return an array of *up to* 3 (maxsplit+1) elements. (In fact, your example only works by accident -- it should be `split("a/b", 1)` to guarantee the call will always succeed.)
Yep, I basically screwed up by misremembering that the count argument to str.split() is a max count, not a guaranteed count. Sorry about the noise on this (although I guess the question somewhat can still be asked had I chosen to create a function that guarantees the length of a list).
-- Teddy
On Mon, Sep 21, 2020 at 12:38 PM Guido van Rossum <guido@python.org> wrote:
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time?
If str.split() worked the way my brain told me it worked, I would have asked if `str.split(self, sep: str, maxsplit: int = Literal[2]) -> SizedList[2, str]: ...` made sense.
-Brett
I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)).
On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/> _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: tsudol@google.com
_______________________________________________
Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: n.a.sobolev@gmail.com
The terminology used by dry-python is hard to follow for me, unfortunately (e.g. "monadic" does nothing for me :-). However there are some people on this list who are working on proposals for tensor types. I don't know if it would apply to the builtin List/list type, but using those proposals you could probably define a function like this ``` def zeros(n: int) -> List[n]: return [0]*n ``` The actual notation being proposed is a bit more complex, but you get the idea. On Tue, Sep 22, 2020 at 10:58 AM Никита Соболев <n.a.sobolev@gmail.com> wrote:
SizedList list is not just a type, it is a dependent type (in a way that the actual type is dependent on the concrete value). That's something very few languages have. And using a language with dependent types is a nightmare for a regular developer.
There are also two projects that can partially solve this problem (based on phantom types, which are just shallow / phantom wrappers for actual types): - https://github.com/antonagestam/phantom-types - https://pypi.org/project/phantoms/ (WIP in our dry-python family)
They have a notation like `NonEmpty[List[int]]`, that guarantees that list has at least one element. And can be extended to use something like `Sized[List[int], 5]` which guarantees that list has specifically 5 elements.
One more thing that might be helpful: monadic `NonEmptyList` type. I am not sure that there are any actual implementations in Python, but we are tracking this potential feature for dry-python/returns here: https://github.com/dry-python/returns/issues/257
вт, 22 сент. 2020 г. в 20:24, Teddy Sudol via Typing-sig < typing-sig@python.org>:
To be clear, my point was that the problem is a lot harder than it looks at first, not just saying your example was bad!
Do other languages have something like SizedList? I can't recall any off the top of my head.
-- Teddy
On Tue, Sep 22, 2020 at 10:21 AM Brett Cannon <brett@python.org> wrote:
On Mon, Sep 21, 2020 at 1:23 PM Teddy Sudol <tsudol@google.com> wrote:
Are you asking for a higher-kinded (I believe?) `split` that can specify in its return type how many elements it returns? A problem with that is `some_str.split(a_delimiter, 2)` is only guaranteed to return an array of *up to* 3 (maxsplit+1) elements. (In fact, your example only works by accident -- it should be `split("a/b", 1)` to guarantee the call will always succeed.)
Yep, I basically screwed up by misremembering that the count argument to str.split() is a max count, not a guaranteed count. Sorry about the noise on this (although I guess the question somewhat can still be asked had I chosen to create a function that guarantees the length of a list).
-- Teddy
On Mon, Sep 21, 2020 at 12:38 PM Guido van Rossum <guido@python.org> wrote:
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time?
If str.split() worked the way my brain told me it worked, I would have asked if `str.split(self, sep: str, maxsplit: int = Literal[2]) -> SizedList[2, str]: ...` made sense.
-Brett
I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)).
On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/> _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: tsudol@google.com
_______________________________________________
Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: n.a.sobolev@gmail.com
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/>
Dependently typed languages (like Idris and ATS) have sized vectors, but they need a proof checker as well as a regular type checker. martin On Tue, Sep 22, 2020 at 10:24 AM Teddy Sudol via Typing-sig < typing-sig@python.org> wrote:
To be clear, my point was that the problem is a lot harder than it looks at first, not just saying your example was bad!
Do other languages have something like SizedList? I can't recall any off the top of my head.
-- Teddy
On Tue, Sep 22, 2020 at 10:21 AM Brett Cannon <brett@python.org> wrote:
On Mon, Sep 21, 2020 at 1:23 PM Teddy Sudol <tsudol@google.com> wrote:
Are you asking for a higher-kinded (I believe?) `split` that can specify in its return type how many elements it returns? A problem with that is `some_str.split(a_delimiter, 2)` is only guaranteed to return an array of *up to* 3 (maxsplit+1) elements. (In fact, your example only works by accident -- it should be `split("a/b", 1)` to guarantee the call will always succeed.)
Yep, I basically screwed up by misremembering that the count argument to str.split() is a max count, not a guaranteed count. Sorry about the noise on this (although I guess the question somewhat can still be asked had I chosen to create a function that guarantees the length of a list).
-- Teddy
On Mon, Sep 21, 2020 at 12:38 PM Guido van Rossum <guido@python.org> wrote:
But in a non-toy example how do you expect a static checker to know how many items "a/b".split("/", 2) returns? Hopefully you're not expecting the checker to evaluate "a/b".split("/", 2) at compile time?
If str.split() worked the way my brain told me it worked, I would have asked if `str.split(self, sep: str, maxsplit: int = Literal[2]) -> SizedList[2, str]: ...` made sense.
-Brett
I could only see making this pass by using cast(Tuple[str, str], "a/b".split("/", 2)).
On Mon, Sep 21, 2020 at 12:15 PM Brett Cannon <brett@python.org> wrote:
Let's say I have the following function:
```python
def spam(a: str, b: str, c: str, d: int = 42): ...
```
Now if I call that with: ```python spam(*"a/b".split("/", 2), "hello") ```
That will execute fine and actually result in appropriate types for those arguments.
Unfortunately both Pylance and mypy say that call is incompatible because of `str.split(...) -> List`. And since 'typing' lacks an concept of a sized list like it does for tuples, I don't know how to make this pass.
Am I overlooking something? Or is this a gap due to there not being an equivalent of 'SizedList' in 'typing'? _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-change-the-world/> _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: tsudol@google.com
_______________________________________________
Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: mdemello@google.com
As Guido has said it is worth mentioning that with the ongoing proposal on type arithmetic it would be possible to do so without theorem proving. (https://docs.google.com/presentation/d/16VGNfVo6Kxk9lBhm1cx1-Jr19dqESyy10Wkh...) However, no matter what way you go it can get tricky when you need to ensure that you will return the size that you are claiming. T = TypeVar("T") L = TypeVar("L", bound = int) K = TypeVar("K", bound = int) class List(Generic[T, L]): ... # Works def append_k(x : List[T,L], k : K) -> List[T, L + K]: result : List[T, L + K] = x + ([0] * k) for i in range(0,k): result[len(x) + 1] = i return result # Doesn't work def append_k(x : List[T,L], k : K) -> List[T, L + K]: result : List[T, L] = list(x) for i in range(0,k): result.append(i) return result The second would not work because of two things. First, because when you call append the type or "result" should change, and the type of a variable cannot change after changing one of its methods. And even if you redeclare the variable in each iteration, you also have the issue that at compile time you don't know how many times will a loop run. Best, Alfonso.
If anyone is curious about how SizedList would look, you can see a gist that works with Pyre: https://gist.github.com/pradeep90/a4e85db014e0e7097f3ebf5ae376846a As Alfonso mentioned, we can't use the default list mutation API with SizedLists (list.append(x)). This is because `append` returns None, so there's no way for us to specify the type of the list after mutation. To use something like SizedList, we would be restricted to a functional API (append(x, sized_list)) or a fluent API (sized_list2 = sized_list.append(x)). One limitation of our current implementation is that we can't typecheck functions like pop_many: ``` def pop_many(xs: SizedList[T, Add[N, M]], n: N) -> SizedList[T, M]: ... xs: SizedList[str, Literal[6]] # Error: Incompatible parameter types... pop_many(xs, 3) ``` This doesn't work because we have to solve for multiple variables N and M in the constraint equations: {N + M = 6, N = 3}. As arithmetic it's pretty basic :), but it would require changing constraint-solving for type variables in general. If there is enough demand for tensor typing and sized lists, we can definitely look into more powerful constraint-solving. (This is all still without needing user-provided proofs.) Best, Pradeep On Wed, Sep 23, 2020 at 4:22 AM Alfonso L. Castaño < alfonsoluis.castanom@um.es> wrote:
As Guido has said it is worth mentioning that with the ongoing proposal on type arithmetic it would be possible to do so without theorem proving. ( https://docs.google.com/presentation/d/16VGNfVo6Kxk9lBhm1cx1-Jr19dqESyy10Wkh... )
However, no matter what way you go it can get tricky when you need to ensure that you will return the size that you are claiming.
T = TypeVar("T") L = TypeVar("L", bound = int) K = TypeVar("K", bound = int)
class List(Generic[T, L]): ...
# Works def append_k(x : List[T,L], k : K) -> List[T, L + K]: result : List[T, L + K] = x + ([0] * k) for i in range(0,k): result[len(x) + 1] = i return result
# Doesn't work def append_k(x : List[T,L], k : K) -> List[T, L + K]: result : List[T, L] = list(x) for i in range(0,k): result.append(i) return result
The second would not work because of two things. First, because when you call append the type or "result" should change, and the type of a variable cannot change after changing one of its methods. And even if you redeclare the variable in each iteration, you also have the issue that at compile time you don't know how many times will a loop run.
Best, Alfonso. _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: gohanpra@gmail.com
As a clarification, I do not quite agree on that we cannot express pop_many in Pyre, it should be so simple as to write: def pop_many(xs: SizedList[T, M], n: N) -> SizedList[T, M - N]: ... Or in current prefix syntax: def pop_many(xs: SizedList[T, M], n: N) -> SizedList[T, Add[M,Mult[N,Literal[-1]]]: ... Best, Alfonso.
Today I found this in TypeScript: https://twitter.com/justinfagnani/status/1309246009017425920 I think that it is highly related. ср, 23 сент. 2020 г. в 16:44, Alfonso L. Castaño <alfonsoluis.castanom@um.es
:
As a clarification, I do not quite agree on that we cannot express pop_many in Pyre, it should be so simple as to write:
def pop_many(xs: SizedList[T, M], n: N) -> SizedList[T, M - N]: ...
Or in current prefix syntax:
def pop_many(xs: SizedList[T, M], n: N) -> SizedList[T, Add[M,Mult[N,Literal[-1]]]: ...
Best, Alfonso. _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: n.a.sobolev@gmail.com
participants (7)
-
Alfonso L. Castaño -
Brett Cannon -
Guido van Rossum -
Martin DeMello -
S Pradeep Kumar -
Teddy Sudol -
Никита Соболев