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