You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
importtorchhelp(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.
The text was updated successfully, but these errors were encountered:
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!
There's been a long history of attempts on typechecking libraries like
einops
,pytorch
andnumpy
. 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: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 (likebeartype
, but statically). Users may use Python code, network requests or arbitrary logic to reason about the type.The text was updated successfully, but these errors were encountered: