Thanks everyone for coming! The recording is available here - we'll hopefully have a link directly to the slides too soon. My attempt at a summary of Elias' talk is:
One thing this approach made me wonder about is, how hard would it be to do something like the following with static type checkers?

def conv2d(input_tensor, kernel_size, stride) -> ProceduralType[conv2d_shape]:
  ...

def conv2d_shape(input_tensor, kernel_size, stride):
  # Computes the return type of conv2d based on x, kernel_size and stride

I'm guessing the main difficulty would be guaranteeing that conv2d_shape really could be understood statically (e.g. that it doesn't depend on global variables)? Iiuc, PyTorch avoids this problem because conv2d_shape is technically written in TorchScript rather than Python - but could we work around this in a different way by e.g. just having the static checker bail out if it finds it can't understand the shape function?

This is of course a separate question to whether we should consider actually doing something like this. In my mind the main argument against it is verbosity: it seems better to keep the whole type signature in one place, rather than having half of it where the function is defined and then the other half in some other function. The downside is that, as Elias pointed out, we probably won't be able to specify the full signature of some operators, e.g. einsum, with only type arithmetic operators - though my current feeling is that's a reasonable tradeoff for the reduction in complexity.

On Wed, 8 Sept 2021 at 10:05, Matthew Rahtz <mrahtz@google.com> wrote:
Alright, so the main item on this month's agenda is that Elias Ellison from the PyTorch dev team will be discussing an approach that PyTorch is planning to use for annotating code with shape information, and how those annotations will be used.

Give me a shout if anyone else has anything to say!

On Tue, 7 Sept 2021 at 17:29, Matthew Rahtz <mrahtz@google.com> wrote:
Hi all,

Our next tensor typing meeting will be Monday the 13th at 6pm London time / 10am San Francisco time at http://meet.google.com/fft-dzjq-ksu. Agenda is yet to be confirmed.

As always, notes and recordings from past meetings are available here.

Thanks!
Matthew