Effects and contracts

This example shows what @ppy.pure refuses, and how a value from a dynamic boundary gets back into typed code.

Run it

python  effects.ppy
ppy     effects.ppy
ppy run effects.ppy

Effects are a set

Every function carries an inferred effect set. I/O, global writes, randomness, time, and mutation of arguments are each tracked on their own. A @ppy.pure decorator is a claim against that set, and the checker either proves it or names the effect that breaks it.

@ppy.pure
def clamp(x: Annotated[int, ppy.Range(0, 255)]) -> Annotated[int, ppy.Range(0, 255)]:
    if x < 0:
        return 0
    if x > 255:
        return 255
    return x

ppy.Range(0, 255) is a refinement the checker propagates. Inside clamp the arithmetic on x needs no overflow guard, and a caller passing 300 is told so at check time.

The other functions in the file:

• scale builds a new list and is pure. Local allocation is fine; mutating an argument is not.
• mix is float arithmetic on f32, pure by construction.
• log_and_total prints, so it carries io. With @ppy.pure on it the checker answers E1601 with the effect named.

The rule is interprocedural. A pure function that calls something with unknown effects is E1602, and a callee that mutates the caller's argument charges the write to the caller.

A boundary for the dynamic part

@ppy.dynamic
def evaluate(source: str) -> int:
    with ppy.dynamic:
        return ppy.check[int](eval(source))

eval is rejected in strict code (E1501). Inside a ppy.dynamic boundary it is allowed, but what comes out is Dynamic, and Dynamic does not fit a declared -> int.

ppy.check[int] validates the value at run time and hands back a typed one. If the value is not an int, it raises TypeError. The boundary suspends the dynamic-feature rules; it does not suspend the types.

What it prints

python effects.ppy, ppy effects.ppy, ppy run effects.ppy

[2.0, 4.0] 255 1.5
1
2
3
42

Read on: Effects and purity · The subset · Dynamic boundaries

effects.ppy is hand-written; there is no .py source and no conversion step.

03_effects_and_contracts/effects.ppy

from typing import Annotated

import ppy
from ppy import f32


@ppy.pure
def scale(values: list[float], factor: float) -> list[float]:
    return [value * factor for value in values]


@ppy.pure
def clamp(x: Annotated[int, ppy.Range(0, 255)]) -> Annotated[int, ppy.Range(0, 255)]:
    if x < 0:
        return 0
    if x > 255:
        return 255
    return x


@ppy.pure
def mix(a: f32, b: f32) -> f32:
    return a * 0.75 + b * 0.25


def log_and_total(values: list[int]) -> int:
    total: int = 0
    for value in values:
        print(value)
        total += value
    return total


@ppy.dynamic
def evaluate(source: str) -> int:
    with ppy.dynamic:
        return ppy.check[int](eval(source))


def main() -> None:
    print(scale([1.0, 2.0], 2.0), clamp(300), mix(1.0, 3.0))
    print(log_and_total([1, 2]))
    print(evaluate("6 * 7"))


if __name__ == "__main__":
    main()

Source: examples/03_effects_and_contracts.