Python可以实现依赖类型吗？

Question

Idris中依赖类型的一个简单演示是Vector，其类型取决于它的值。在

我们可以用Python定义类型提示。在

from typing import List

def append(a: List[int], b: List[int]) -> List[int]:
    return a + b

print(append([1, 2], [1, 3, 4]))

那么，我们能否实现一个Vect类型，它可以如下使用：

^{pr2}$

m和n是自然数，t是任何类型的。在