Calculated types, custom types and type checkers

[chatgpt-api-cn]

There's been a long history of attempts on typechecking libraries like einops, pytorch and numpy. One major issue is that passing different parameters to these constructors create different types (tensors with traits (matrix multiplication) and tensor functions). There's some relationship between definition of a convolutional network and what type of value (usually not a fixed type, but rather a set of types (infinite)) it can accept and return.

So I propose or want to know how we can let Erg to solve this long-standing problem, by letting the static typechecker to know the type of torch.nn.Conv2d and emit errors before execution? Help can be found by:

import torch
help(torch.nn.Conv2d)

Calculated types

More than traditional computer type theory (invariant, covariant, etc.), just like what Erg defines Nat (natural numbers), users can use calculated type to construct new types and a set of types by reading parameters from constructors, code context and more. This brings symbolic algebra (sympy) to life, so type checking might also become equation solving.

Custom type checker

Let the user to define (like Annotated in Python) and check types (like beartype, but statically). Users may use Python code, network requests or arbitrary logic to reason about the type.

[mtshiba]

Yes, in fact one of Erg's motivations for introducing dependent types is to be able to verify array and tensor transformations at compile time. I am currently trying to have the information of numpy.ndarray.shape in the type as a start. Stay tuned!