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
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
wrote: On Wed, May 19, 2021 at 2:37 PM Guido van Rossum
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