Scott encoding maxed out

scott.py

from __future__ import annotations

import builtins
from typing import Protocol


class Ty[T]:
    pass


type Type[T] = type[Ty[T]]


class Bool(Protocol):
    def __call__[R](self, r: Type[R], /) -> BoolR[R]: ...


class BoolR[R](Protocol):
    def __call__(self, no: R, /) -> BoolNo[R]: ...


class BoolNo[R](Protocol):
    def __call__(self, yes: R, /) -> BoolYes[R]: ...


type BoolYes[R] = R


def no[R](r: Type[R]) -> BoolR[R]:
    def no_r(no: R) -> BoolNo[R]:
        def no_no(yes: R) -> BoolYes[R]:
            return no

        return no_no

    return no_r


def yes[R](r: Type[R]) -> BoolR[R]:
    def yes_r(no: R) -> BoolNo[R]:
        def yes_no(yes: R) -> BoolYes[R]:
            return yes

        return yes_no

    return yes_r


def from_builtin_bool(bool: builtins.bool) -> Bool:
    return yes if bool else no


def to_builtin_bool(bool: Bool) -> builtins.bool:
    return bool(Ty[builtins.bool])(False)(True)


def either(second: Bool) -> EitherSecond:
    def either_second(first: Bool) -> Bool:
        return first(Ty[Bool])(second)(yes)

    return either_second


class EitherSecond(Protocol):
    def __call__(self, first: Bool, /) -> Bool: ...


def both(second: Bool) -> BothSecond:
    def both_second(first: Bool) -> Bool:
        return first(Ty[Bool])(no)(second)

    return both_second


class BothSecond(Protocol):
    def __call__(self, first: Bool, /) -> Bool: ...


def negate(bool: Bool) -> Bool:
    return bool(Ty[Bool])(yes)(no)


def same(second: Bool) -> SameSecond:
    def same_second(first: Bool) -> Bool:
        return first(Ty[Bool])(negate(second))(second)

    return same_second


class SameSecond(Protocol):
    def __call__(self, first: Bool, /) -> Bool: ...


def different(second: Bool) -> DifferentSecond:
    def different_second(first: Bool) -> Bool:
        return first(Ty[Bool])(second)(negate(second))

    return different_second


class DifferentSecond(Protocol):
    def __call__(self, first: Bool, /) -> Bool: ...


def main() -> None:
    to_be_or_not_to_be = yes
    print(to_be_or_not_to_be(Ty[str])("not to be")("to be"))


main()