-
-
Notifications
You must be signed in to change notification settings - Fork 53
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Calculated types, custom types and type checkers #445
Labels
enhancement
New feature or request
Comments
chatgpt-api-cn
changed the title
Calculated types or custom type hint and type checkers
Calculated types, custom types and type checkers
Jul 27, 2023
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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: