There are a few efforts working in this space. As you can imagine, all of them are experimental:

- Dex: https://github.com/google-research/dex-lang/ - Hasktorch: https://github.com/hasktorch/hasktorch - This initiative from the Python Typing-sig: https://docs.google.com/document/d/1oaG0V2ZE5BRDjd9N-Tr1N0IK...

Futhark has size types,

https://futhark-lang.org/blog/2020-03-15-futhark-0.15.1-rele...

and it seems to be ok for DL

https://elsman.com/pdf/fhpnc19.pdf

This is not statically checked but it's a step in the right direction: https://pytorch.org/docs/stable/named_tensor.html

Yeah, I actually helped work on the inspo for that project https://github.com/harvardnlp/namedtensor .

From what I've been able to tell, (no shade to the Pytorch team which has many different priorities) work has been somewhat slow going on the port.

Further, this is dynamic type checking as you mentioned.

I see, interesting! Yeah statically checking this would be way more awesome still

Oh I just noticed that you're one of the people behind that recent GAN compression work! Really cool stuff and a big step up this year, I've been following the field for a lil bit.

Congrats!

Thanks a lot for the kind words!