Support for type checking fixed width integers
I'm aware that the python3 type system primarily supports arbitrary precision integers and there is no support for type checking fixed width integers. However, when python is used as an approachable first language for data scientists, scientists interested in numerical analysis and possibly other generic use cases, one common technique is to map python's type system to that of a lower level underlying system. I'm primarily coming at it from the third use case in the form of py2many, a transpiler for converting python to many statically typed C-like languages. I suspect pytorch, tensorflow or anything that maps python to vectorized hardware efficiently has to deal with the precision of integers. Canonical use case: ``` #!/usr/bin/env python3 from ctypes import c_int8 as i8 def test(): a: i8 = 10 b: i8 = 20 c = a + b reveal_type(c) ``` Also would love to have type checkers infer ranges and throw errors for cases like: c: i8 = 300 Doing so would significantly benefit the use case of generating secure C++/Rust code from python source: https://github.com/adsharma/py2many/issues/233 Eric Traut suggested I post to the mailing list. More context here: https://github.com/microsoft/pyright/issues/1872 -Arun
How well would something like this solve your issue? import typing if typing.TYPE_CHECKING: class i8(int): pass else: from ctypes import c_int8 as i8 Or perhaps instead of the class definition use a type alias: i8 = int On Wed, May 19, 2021 at 1:59 PM Arun Sharma <arun@sharma-home.net> wrote:
I'm aware that the python3 type system primarily supports arbitrary precision integers and there is no support for type checking fixed width integers.
However, when python is used as an approachable first language for data scientists, scientists interested in numerical analysis and possibly other generic use cases, one common technique is to map python's type system to that of a lower level underlying system.
I'm primarily coming at it from the third use case in the form of py2many, a transpiler for converting python to many statically typed C-like languages. I suspect pytorch, tensorflow or anything that maps python to vectorized hardware efficiently has to deal with the precision of integers.
Canonical use case:
``` #!/usr/bin/env python3
from ctypes import c_int8 as i8
def test(): a: i8 = 10 b: i8 = 20 c = a + b reveal_type(c) ```
Also would love to have type checkers infer ranges and throw errors for cases like:
c: i8 = 300
Doing so would significantly benefit the use case of generating secure C++/Rust code from python source:
https://github.com/adsharma/py2many/issues/233
Eric Traut suggested I post to the mailing list. More context here:
https://github.com/microsoft/pyright/issues/1872
-Arun
_______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: guido@python.org
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-c...>
On Wed, May 19, 2021 at 2:37 PM Guido van Rossum <guido@python.org> wrote:
How well would something like this solve your issue?
import typing if typing.TYPE_CHECKING: class i8(int): pass else: from ctypes import c_int8 as i8
This approach has the benefit of avoiding a common problem with the c_int8 approach. a: i8 = i8(1) b: i8 = i8(2)
a + b TypeError: unsupported operand type(s) for +: 'c_byte' and 'c_byte'
I generally like it (as long as they're builtin/ergonomic and end users don't have to write the imports). But code such as: a: i8 = 1 b: i8 = 2 c: int = a + b generate errors that I would like to see go away
Or perhaps instead of the class definition use a type alias:
i8 = int
a: i8 = 10 b: i16 = 20 a = b # should generate an error but doesn't. -Arun
https://github.com/adsharma/py2many/pull/254 implements some of this. Before transpiling, if we detect such overflows the transpiler errors out instead of relying on the target language compiler to report it. TODO: Do something similar for underflows. -Arun On Wed, May 19, 2021 at 3:04 PM Arun Sharma <arun@sharma-home.net> wrote:
On Wed, May 19, 2021 at 2:37 PM Guido van Rossum <guido@python.org> wrote:
How well would something like this solve your issue?
import typing if typing.TYPE_CHECKING: class i8(int): pass else: from ctypes import c_int8 as i8
This approach has the benefit of avoiding a common problem with the c_int8 approach.
a: i8 = i8(1) b: i8 = i8(2)
a + b TypeError: unsupported operand type(s) for +: 'c_byte' and 'c_byte'
I generally like it (as long as they're builtin/ergonomic and end users don't have to write the imports). But code such as:
a: i8 = 1 b: i8 = 2 c: int = a + b
generate errors that I would like to see go away
Or perhaps instead of the class definition use a type alias:
i8 = int
a: i8 = 10 b: i16 = 20
a = b # should generate an error but doesn't.
-Arun
I have a fork of Typpete here: https://github.com/adsharma/Typpete/ that improves usability and commit 38068ca adds support for type checking fixed width integers. i: u8 = 300 # generates a type error General idea: use a type hierarchy such as: complex -> float -> int -> i64 -> i32 -> i16 -> i8 -> bool Things I'm looking to implement: * axioms for overflow, underflow detection and type inference * dependent and refinement types (which is basically a generalization of the above commit) * Requires/ensures for functions based on types. Looking for collaborators and people more familiar with z3 than I am. -Arun On Sun, May 23, 2021 at 11:06 AM Arun Sharma <arun@sharma-home.net> wrote:
https://github.com/adsharma/py2many/pull/254 implements some of this. Before transpiling, if we detect such overflows the transpiler errors out instead of relying on the target language compiler to report it.
TODO: Do something similar for underflows.
-Arun
On Wed, May 19, 2021 at 3:04 PM Arun Sharma <arun@sharma-home.net> wrote:
On Wed, May 19, 2021 at 2:37 PM Guido van Rossum <guido@python.org> wrote:
How well would something like this solve your issue?
import typing if typing.TYPE_CHECKING: class i8(int): pass else: from ctypes import c_int8 as i8
This approach has the benefit of avoiding a common problem with the c_int8 approach.
a: i8 = i8(1) b: i8 = i8(2)
a + b TypeError: unsupported operand type(s) for +: 'c_byte' and 'c_byte'
I generally like it (as long as they're builtin/ergonomic and end users don't have to write the imports). But code such as:
a: i8 = 1 b: i8 = 2 c: int = a + b
generate errors that I would like to see go away
Or perhaps instead of the class definition use a type alias:
i8 = int
a: i8 = 10 b: i16 = 20
a = b # should generate an error but doesn't.
-Arun
participants (2)
-
Arun Sharma -
Guido van Rossum