Use plugin to support numpy

[JukkaL]

This was originally discussed at #1240. It's unclear how this would work exactly -- we may first need to design a static type system extension for numpy.

[ilevkivskyi]

we may first need to design a static type system extension for numpy.

I think we would only need some dependent type to describe a fixed size array Array[np.foat32, n, k], where n and k are integer numbers known statically. Related #3062 and #3345

[kmike]

This project looks somewhat related: http://datashape.readthedocs.io, https://github.com/blaze/datashape

[mrocklin]

There is some conversation about type annotations in this NumPy issue: numpy/numpy#7370

[shoyer]

Here's my brain dump on static typing for arrays:

TensorFlow (which copies the design of NumPy in many ways) has a form of static typing for array shapes that is useful precedence here. Notably, it distinguishes between three cases (copied from that page):

• Fully-known shape: has a known number of dimensions and a known size for each dimension. e.g. TensorShape([16, 256])
• Partially-known shape: has a known number of dimensions, and an unknown size for one or more dimension. e.g. TensorShape([None, 256])
• Unknown shape: has an unknown number of dimensions, and an unknown size in all dimensions. e.g. TensorShape(None)

TensorFlow sets shapes using C++ or Python, mostly with SetShapeFn. Looking through how it's used internally by TensorFlow operations could give hints about the necessary use cases.

In particular, one important use case supported by most NumPy functions is broadcasting, where output shapes are propagated via broadcasting rules. This could allow for identifying broadcasting errors (one of the most frequent user-errors in NumPy) at compile-time instead of run-time.

Finally, a concept like TypeVar for arrays dimensions (call it DimensionVar?) could be extremely powerful. In NumPy, an operation like x + y for inputs x: Vector[N] and y: Vector[M] only can succeed if N=1, M=1 or N=M. Obviously, this is error prone -- N and M can coincide purely by chance, even if they represent semantically distinct axes. For static checking, it could be useful to assume that N and M are always distinct, unless cast to use the same dimension variables. This would also catch many errors.

[mitar]

I think we would only need some dependent type

I think dependent types are needed in very rare cases. What we probably need more, is something like static constraints. So dependent types would mean that some part of the type is based on value of function argument. For example, if function would be:

def foo(array, array_dtype):
    ...

Where array has dtype of array_dtype, then you would need a dependent type to express that array argument has numpy type with array_dtype as its dtype.

But what we first need is even support to express "numpy with dtype" type. I see this as an extra constraint on numpy type. The issue is that it is not enough just to have support for static constraints, but one needs a language so that you can describe that input arguments to a function can have some relations between them (like one argument array has to be 2x in width than the other argument array). It gets pretty tricky soon. See contracts project for an attempt at this.

[petered]

Working on a large codebase of scientific python code, a generic array-type annotation would be incredibly useful. An example that would be nice to type-check:

def compute_costs(
    predictions,  # type: Array(n_samples, n_outputs)[float]   # Array of probabilities
    labels,  # type: Array(n_samples)[int,>=0,<n_outputs]  # Correct labels in range 0 to n_outputs-1
):  # type: (...) -> Array(n_samples)[float]  # The cost per-sample

This documents that:

• The predictions and the labels must have the same number of samples
• The returned costs has the same number of samples as predictions
• The elements in labels should not exceed the dimensions of predictions.

It would be good to add more flexibility to this example. For example it may be the case that the data points are not flattened along one dimension, e.g.

def compute_costs(
    predictions,  # type: Array(n_samples, *data_dims, n_outputs)[float]   # Array of probabilities
    labels,  # type: Array(n_samples, *data_dims)[int,>=0,<n_outputs]  # Correct labels in range 0 to n_outputs-1
):  # type: (...) -> Array(n_samples)[float]  # The cost per-sample

This would indicate that the predictions and labels can have any shapes as long as they match.

It would also be great to have some kind of support for Generics Types. For example:

def minibatch_iterator(
   data_iterator,  # type: Generator[Array(*dims)[<dtype>]],
   minibatch_size,  # type: int
):  # type: (...) -> Generator[Array(minibatch_size, *dims)[<dtype>]],

This annotation would show that

• The first dimension of the yielded arrays would match the minibatch size, and the remaining dimensions would match whatever comes out of the data iterator
• The type would match whatever comes out of the data iterator.

[JelleZijlstra]

FYI, the https://github.com/numpy/numpy_stubs project is now working on support for typing numpy-using code.

[shoyer]

Yes, and we are very much interested in collaboration. See here for ongoing discussion about typing shapes: https://github.com/numpy/numpy_stubs/issues/5

[gvanrossum]

Who is "we" here and who do you want to collaborate with? Is there a complete proposal for the syntax yet? It would have to aim at becoming a PEP (a sibling to PEP 484 and PEP 526) and someone should attempt an implementation for mypy, perhaps in the form of a plugin. The mypy team doesn't have the resources or priorities to help much, alas.