Integer generics

No implementation files or tests are named. Start by reading the related issues #366 and #3062 and the referenced typing and Rust discussions, then determine whether integer generics fit mypy's type system; done would require an agreed design and implementation scope rather than only discussion.

Dependent types have been brought up before in a few places: #366, this python-ideas thread, and most recently, #3062. The latter limits itself to one specific feature of a dependent type system, namely, support for simple literal types.

Another limited feature which could prove helpful is support for integer generics —that is, the ability to parametrize types by integers as well as other types. For example, the length of a homogeneous tuple could be parametrized:

# Currently supported:
Tuple[int, int, int] # A tuple of 3 ints
Tuple[int, ...] # A tuple of any number of ints

# Proposed:
Tuple[int, 256] # A tuple of 256 ints

One real-world use-case for this came up in python/typing#221:

# Currently supported:
SboxType = Tuple[
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
    Tuple[int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int],
]

# Proposed:
SboxType = Tuple[Tuple[int, 16], 8] # A tuple of 8 tuples of 16 ints each

Integer genericity could also be used for things like statically checking vector or matrix dimensions:

N = TypeVar('N', numeric=True) # one idea for denoting type-level integers

class Vector(Generic[N]):
    def __init__(self, values: Iterable[float, N]) -> None:
        self.value = tuple(values)

    def __add__(self, other: Vector[N]) -> Vector[N]:
        return Vector(a + b for a, b in zip(self.values, other.values))

# ...more code...

def matmul(a: Matrix[N, M], b: Matrix[M, D]) -> Matrix[N, D]: ...

Note that the Rust community has been discussing this for some time (as well as the more general const generics) and has a lot of material collected on the motivation, challenges, and details of such a feature:

• Pre-RFC: Integer Templating
• rust-lang/rfcs#1038: Parameterize types over numerics / type level integers
• rust-lang/rfcs#1931: RFC: Constant generics (restricted Π types) for Rust, core RFC (v2)
• [lang-team-minutes] Const generics

Whether or not it's a good fit for Python is an open question, of course, but I figured I should at least bring it up for discussion! (Especially since it could interact with #3062 in interesting ways.)

(Even nicer would be to support simple type-level expressions so we could do things like this...

# Vector concatenation (relevant: http://stackoverflow.com/q/43292197/1974654)
def concat(a: Vector[N], b: Vector[M]) -> Vector[N+M]: ...

# The `zip` builtin (based on the typeshed stub)
@overload
def zip(iter1: Iterable[_T1, N1],
        iter2: Iterable[_T2, N2]) -> Iterator[Tuple[_T1, _T2], min(N1, N2)]: ...

# HDL-like bit vector operations
def add(a: BitVec[N], b: BitVec[M]) -> BitVec[max(N, M) + 1]: ...

...but that may be taking it too far. To avoid running arbitrary user code the expression language would have to be explicitly defined and simple enough to implement in languages other than Python; it may be feasible to support something like +, -, *, //, %, **, max(), min(), and abs(), though.)