Skip to content

type-time functions #258

@KotlinIsland

Description

@KotlinIsland

functions that will be run at type-time. similar to plugins, but don't care about mypy internals.

ideally:

@type_function
def Add(left: int, right: int) -> int:
    return left + right

type A = 1
type B = 2
type C = Add[A, B]

reveal_type(C)  # 3

it would typecheck as if it's a normal function with values

type D = Add[int, 2]  # `Add`s first parameter expects an int, found type[int]

it would accept arbitrary types:

@type_function
def MapIntTo(In: object, To: object) -> In | To:
    if issubclass(In, int) or isinstance(In, int):
        return To
    # TODO: handle unions
    return In
      

def f[T](t: T) -> MapIntTo[T, str]: ...

f(1)  # str
f(None)  # None

it would be composable:

@type_function
def Extends(Value: object, Type: object) -> bool:
   # TODO: handle classes, unions etc
    return isinstance(Value, Type)

@type_function
def If(Condition: bool, IfTrue, IfFalse):
    if Condition:
        return IfTrue
    return IfFalse

def f[T](t: T) -> If[Extends[T, int], str, T]: ...

f(1)  # str
f(None)  # None

it could be inline:

def trim[T: str](t: T) -> type_function[lambda T: T[:3] if isinstance(T, str) else T]: ...

trim("abcd")  # "abc"

it would be able to raise TypeError:

@type_function
def NotNone[T](Type: T | None) -> T:
    if Type is NoneType or isinstance(Type, UnionType) and NoneType in Type.__args__:
        raise TypeError("`None` is incompatible with this")
        # OR, not sure which one makes more sense
        return TypeError("`None` is incompatible with this")

def f[T](t: NotNone[T]): ...

f(None) # error: `None` is incompatible with this  [type-function]

BONUS: single argument functions would be able to automatically capture the corresponding type

@type_function
def NotNone[T](Type: T | None) -> T: ...        

def f(t: NotNone): ...

a: int | None
f(a)  # error: `None` is incompatible with this  [type-function]

@type_function
def Thing(Type: object) -> object:
    if Type == "a":
        raise TypeError("fail...")
    return Type

def f2() -> Thing:
    if bool(): return 1
    return "a"  # fail...

Related #249

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions