Python mechanisms used by the library¶

Basic Python syntax is assumed. This preparation chapter explains the data model and metaprogramming that make the mathematical notation meaningful.

Why start here?

Later chapters ask you to connect a definition to +, ==, a dataclass option, or a decorator. None of those connections requires guessing once Python's dispatch rules are explicit.

By the end, you can explain

why a + b normally starts at a.__add__(b);
how @log replaces a function with a wrapper;
which dataclass methods are generated and which this project suppresses;
why a passing test is evidence about code, not a general proof.

Source used in this chapter

Open the complete logging implementation and its tests when you need the context around an excerpt.

Operators are method dispatch¶

For a user-defined object, left + right asks the left operand to handle the operation:

left + right
    ↓
left.__add__(right)
    ↓
result, or NotImplemented

NotImplemented is a special return value, not an exception. It tells Python that this method does not know the other operand and allows reflected dispatch, such as right.__radd__(left), to continue. This becomes important when values from different levels of the numeric tower interact.

Notation does not hide the implementation

In this course, reading n + m means locating type(n).__add__, then following its branches.

A decorator changes the public callable¶

This is the central part of @log:

def outer(func):
    @wraps(func)
    def inner(*args, **kwargs):
        result, message = func(*args, **kwargs)
        if logger.isEnabledFor(log_level):
            logger.log(
                log_level,
                message if isinstance(message, str) else message(),
            )
        return result
    return inner

Writing @log(log_level=4) above __add__ is equivalent to assigning the result of the decorator back to the same name:

NaturalNumber.__add__ = log(log_level=4)(original_add)

The original method returns (result, message_factory). Callers see inner, which returns only result. The factory is a zero-argument function so the message is not built when tracing is disabled.

@wraps preserves identity

A wrapper would otherwise appear to be named inner. @wraps(func) preserves the original name, documentation, and a link to the wrapped function. This project additionally rewrites the public return annotation from the internal tuple type to the result type.

Dataclass generation is selective¶

@dataclass(frozen=True, slots=True, eq=False, repr=False)
class NaturalNumber:
    pre: NaturalNumber | None = None

Here the dataclass generates initialization, but:

frozen=True prevents field reassignment after construction;
slots=True prevents undeclared instance fields;
eq=False leaves equality to the hand-written Peano rules;
repr=False leaves structural display to the library.

Other classes use __post_init__ to validate generated initialization. Polynomial uses init=False and writes its own initializer because normalization must happen before coefficients are stored.

Generated code is still part of the design

Each option decides which behavior Python supplies and which behavior must remain visible in the mathematical implementation.

Tests check executable claims¶

The logging tests inspect both the public signature and the emitted trace:

def test_decorator_preserves_method_metadata(self) -> None:
    self.assertEqual(N_ONE.__add__.__name__, "__add__")
    self.assertTrue(hasattr(N_ONE.__add__, "__wrapped__"))

Test and theorem are different claims

This test can detect a broken wrapper for the specific implementation. It does not prove a property of all decorators. Later arithmetic tests have the same boundary: they protect representative laws without replacing a proof by induction.

Predict the call boundary

If an internal decorated method returns (3, message_factory), what does the caller receive, and when is the factory invoked?

You now have the vocabulary needed to read the first construction without assuming any prior knowledge of its source.

Next: construct natural numbers from zero and successor →