Last active
June 25, 2024 12:23
-
-
Save hanshoglund/d255b3a9ff0a07cf7504a3b4313d6d7c to your computer and use it in GitHub Desktop.
adts3.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 typing import Generic, TypeVar, final | |
from typing import Callable | |
from dataclasses import dataclass | |
L = TypeVar("L") | |
R = TypeVar("R") | |
class Either(Generic[L,R]): ... | |
@final | |
@dataclass(frozen=True) | |
class Left(Either[L,R]): | |
val: L | |
@final | |
@dataclass(frozen=True) | |
class Right(Either[L,R]): | |
val: R | |
A = TypeVar("A") | |
def either(l: Callable[[L], A], r: Callable[[R], A], e: Either[L,R]) -> A: | |
match e: | |
case Left(x): | |
return l(x) | |
case Right(y): | |
return r(y) | |
assert False | |
# either(lambda x: print(x + 1), lambda y: print(y + "_"), Left(2)) # falsely rejected by mypy 1.8.0 | |
# either(lambda x: print(x + 1), lambda y: print(y + "_"), Right("hi")) # correctly accepted by mypy 1.8.0 | |
# either(lambda x: print(x + 1), lambda y: print(y + "_"), Right(2)) # correctly rejected by mypy 1.8.0 | |
# either(lambda x: print(x + 1), lambda y: print(y + "_"), Left("hi")) # correctly rejected by mypy 1.8.0 | |
def pr_l(x: int):... | |
def pr_r(x: str):... | |
either(pr_l, pr_r, Left(23)) | |
either(pr_l, pr_r, Right("")) | |
# either(pr_l, pr_r, Right(23)) # correctly rejected | |
# either(pr_l, pr_r, Left("")) # correctly rejected |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment