Example SizedList type in Pyre

sized_list.py

from typing import *
from typing_extensions import Literal
from pyre_extensions import Add

T = TypeVar("T")
N = TypeVar("N", bound=int)
M = TypeVar("M", bound=int)


class SizedList(Generic[T, N]): ...

def repeat(x: T, n: N) -> SizedList[T, N]: ...

def append(x: T, xs: SizedList[T, N]) -> SizedList[T, Add[N, Literal[1]]]: ...
    
def pop(xs: SizedList[T, Add[N, Literal[1]]]) -> SizedList[T, N]: ...

def zeros(n: N) -> SizedList[int, N]:
    zero: int
    return repeat(zero, n)

str1: str
str2: str

# Revealed type is `SizedList[int, Literal[3]]`.
reveal_type(zeros(3))
# Revealed type is `SizedList[int, Literal[4]]`.
reveal_type(append(7, zeros(3)))

# No error.
z = append(str1, repeat(str2, 5))
# Revealed type for `z` is `SizedList[str, Literal[6]]`.
reveal_type(z)

# Error: Incompatible parameter type!
append(str1, repeat(3, 5))


# Revealed type is SizedList[str, Literal[5]].
reveal_type(pop(z))
# Revealed type is SizedList[str, Literal[4]].
reveal_type(pop(pop(z)))




# Limitations:

def pop_many(xs: SizedList[T, Add[N, M]], n: N) -> SizedList[T, M]: ...

# Error: Expected SizedList[T, Add[N, M]] but got SizedList[str, Literal[6]].
pop_many(z, 3)

# This doesn't work with our current proposal because we have to infer N and M from the constraints: {N + M = 6, M = 3}.

Needs https://pypi.org/project/pyre-extensions/