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