Towards Dependent Types - An Actual Use Case

[randolf-scholz]

Dependent types have been discussed before (#366, #3062). I am currently dealing with an actual use case where something like the TypeMapping proposed here #3062 (comment) would be really useful.

That is, I am writing code for Time-Series Data Analysis that is relatively generic and could potentially support a variate of different datetime and timedelta formats out there, such as:

• datetime.datetime / datetime.timedelta
• numpy.datetime64 / numpy.timedelta64
• pandas.Timestamp / pandas.Timedelta
• int/int or float/float

Crucially, an issue that makes it complicated to provide generic type hints is that the timedelta-type should be compatible with the datetime type. If one of them comes from the pandas family, the other should as well.

Example function:

def grid(
    tmin: DT, tmax: DT, timedelta: TD, offset: Optional[DT] = None
) -> list[int]:
    r"""Compute $\{k∈ℤ∣ tₘᵢₙ ≤ t₀+k⋅Δt ≤ tₘₐₓ\}$."""
    offset = tmin if offset is None else offset
    zero_dt = tmin - tmin  # generates zero variable of correct type
    assert timedelta > zero_dt,    "Assumption delta>0 violated!"
    assert tmin <= offset <= tmax, "Assumption: xmin≤xoffset≤xmax violated!"

    a = tmin - offset
    b = tmax - offset
    kmax = int(b // timedelta)  # need int() in case both are floats
    kmin = int(a // timedelta)
    return list(range(kmin, kmax + 1))

This function does indeed work with all the types mentioned above. And in principle, we could solve the type-hinting problem here by doing a bunch of @overloads.

Though, the problem starts to become bigger when we start talking about writing lots of these generic functions or classes with multiple methods.

Proposal

Apart from the TypeMapping suggested here #3062 (comment), another possibility could be to introduce an additional syntax for @overload similar to how @pytest.mark.parametrize works, i.e.

ValidTypePairs = TypeList[
    TypeTuple[int, int],
    TypeTuple[float, float],
    TypeTuple[datetime, timedelta],
    TypeTuple[np.datetime64, np.timedelta64],
    TypeTuple[pd.Timestamp, pd.Timedelta],
]

@overload("DT,TD", ValidTypePairs)
def grid(
    tmin: DT, tmax: DT, timedelta: TD, offset: Optional[DT] = None
) -> list[int]:
    ...

[harahu]

Am having the exact same issue, with the exact same time-related types. Good suggestion!

EDIT: Although, you might want to propose this to the people over at https://github.com/python/typing instead.

[AlexWaygood]

EDIT: Although, you might want to propose this to the people over at https://github.com/python/typing instead.

Yeah, feature requests that affect the typing community as a whole don't belong in this repo. There are lots of other type checkers, so if you want to change the spec in some way, you should start a discussion at https://github.com/python/typing or the typing-sig mailing list