Created
February 8, 2025 08:42
-
-
Save decorator-factory/8939a2c8f380070ba762916fcc2fdab2 to your computer and use it in GitHub Desktop.
poople.py
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from __future__ import annotations | |
from collections.abc import Callable | |
from typing import final, Any | |
type Peano = S[Any] | Z | |
@final | |
class S[T: Peano]: pass | |
@final | |
class Z: pass | |
N1 = S[Z] | |
N2 = S[N1] | |
N3 = S[N2] | |
N4 = S[N3] | |
N5 = S[N4] | |
class Poople[N: Peano, T]: | |
def __init__(self: Poople[Z, T]) -> None: ... # type: ignore | |
def add(self, item: T) -> Poople[S[N], T]: ... | |
def map[U](self, fn: Callable[[T], U]) -> Poople[N, U]: ... | |
class Poopler[N: Peano, T, *Rest]: | |
def __init__(self: Poopler[N1, T, *Rest], t: tuple[T, *Rest]) -> None: ... # type: ignore | |
def slurp[*Others](self: Poopler[N, T, T, *Others]) -> Poopler[S[N], T, *Others]: ... | |
def done(self: Poopler[N, T]) -> Poople[N, T]: ... | |
class Unpoopler[N: Peano, T, Out: tuple[object, ...]]: | |
def __init__(self: Unpoopler[N, T, tuple[()]], poople: Poople[N, T]) -> None: # type: ignore | |
... | |
def slurp[M: Peano, *Xs]( | |
self: Unpoopler[S[M], T, tuple[*Xs]] | |
) -> Unpoopler[M, T, tuple[T, *Xs]]: ... | |
def done(self: Unpoopler[Z, T, Out]) -> Out: ... | |
# unpoopler | |
def extract_pair(p: Poople[N2, int]) -> tuple[int, int]: | |
return Unpoopler(p).slurp().slurp().done() | |
def extract_wrong1(p: Poople[N2, int]) -> tuple[int, int]: | |
# `p` is a pair, so `Unpoopler(p).slurp()` is an `Unpoopler[N1, int, tuple[int]]` | |
# but `done` requires that the first parameter is Z | |
return Unpoopler(p).slurp().done() | |
def extract_wrong2(p: Poople[N3, int]) -> tuple[int, int]: | |
# `p` is a triple, so `Unpoopler(p).slurp().slurp()` is an `Unpoopler[N1, int, tuple[int, int]]` | |
# but `done` requires that the first parameter is Z | |
return Unpoopler(p).slurp().slurp().done() | |
def extract_wrong3(p: Poople[N3, int]) -> tuple[int, int]: | |
# tuple[int, int, int] is not assignable to tuple[int, int] | |
return Unpoopler(p).slurp().slurp().slurp().done() | |
def extract_quintuple(p: Poople[N5, str]): | |
# hover over `extract_quintuple` to see inferred type | |
return Unpoopler(p).slurp().slurp().slurp().slurp().slurp().done() | |
reveal_type(extract_quintuple) # returns the correct tuple type | |
# poopler | |
def construct_zero() -> Poople[Z, bool]: | |
return Poople() | |
def construct_one(p: tuple[bool]) -> Poople[N1, bool]: | |
return Poopler(p).done() | |
def construct_pair(p: tuple[bool, bool]) -> Poople[N2, bool]: | |
return Poopler(p).slurp().done() | |
def construct_triple(p: tuple[bool, bool, bool]) -> Poople[N3, bool]: | |
return Poopler(p).slurp().slurp().done() | |
def construct_wrong1(p: tuple[bool, bool]) -> Poople[N2, bool]: | |
return Poopler(p).done() | |
def construct_wrong2(p: tuple[bool, bool, bool]) -> Poople[N2, bool]: | |
return Poopler(p).slurp().done() | |
def construct_wrong3(p: tuple[bool, bool, bool]) -> Poople[N3, bool]: | |
return Poopler(p).slurp().done() | |
def construct_wrong4(p: tuple[int, bool, bool]) -> Poople[N3, bool]: | |
return Poopler(p).slurp().slurp().done() | |
def construct_wrong5(p: tuple[bool, int, bool]) -> Poople[N3, bool]: | |
return Poopler(p).slurp().slurp().done() | |
def construct_wrong6(p: tuple[bool, bool, int]) -> Poople[N3, bool]: | |
return Poopler(p).slurp().slurp().done() | |
def construct_quinpoople(p: tuple[str, str, str, str, str,]) | |
return Poopler(p).slurp().slurp().slurp().slurp().done() | |
reveal_type(construct_quinpoople) # returns the correct Poople type | |
### | |
class SensorHub: | |
def _get_sensor_value(self, sensor_name: str) -> float: | |
return len(sensor_name)**0.5 | |
def collect_measurement[N: Peano](self, sensor_names: Poople[N, str]) -> Poople[N, float]: | |
return sensor_names.map(self._get_sensor_value) | |
hub = SensorHub() | |
sensors = ("heat_c", "pressure_atm", "sound_db") | |
_ = hub.collect_measurement(Poopler(sensors).done()) # error | |
_ = hub.collect_measurement(Poopler(sensors).slurp().done()) # error | |
j = hub.collect_measurement(Poopler(sensors).slurp().slurp().done()) # no error! | |
reveal_type(j) # Poople[S[S[S[Z]]], str] | |
_ = Unpoopler(j).done() # error | |
_ = Unpoopler(j).slurp().done() # error | |
_ = Unpoopler(j).slurp().slurp().done() # error | |
readings = Unpoopler(j).slurp().slurp().slurp().done() # no error! | |
reveal_type(readings) # here's our tuple[float, float, float] readings! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment