A tour of Pagda

Eleven short programs. Each was run to build this page, and the panel under it shows what pagda printed. Every file starts with the two lines from Get started; the Copy button includes them.

An ordinary program

A checked file looks like typed Python. Every def says what it takes and what it gives back. A class with fields is a @dataclass.

t01_hello.pychecked

@dataclass
class Item:
    name: str
    price: int
    count: Nat


def total(items: list[Item]) -> int:
    t = 0
    for item in items:
        t += item.price * item.count
    return t


def main() -> None:
    stock = [Item("pen", 3, 10), Item("ink", 12, 2)]
    for item in stock:
        print(f"{item.name}: {item.price} x {item.count}")
    print("total", total(stock))


if __name__ == "__main__":
    main()

$ pagda t01_hello.py

pen: 3 x 10
ink: 12 x 2
total 54

Two number types appear here. int is any whole number. Nat is 0, 1, 2 and up, the type of counts and positions. A Nat is accepted wherever an int is wanted.

Things that can fail

Reading xs[i] fails when i is past the end. Dividing fails when the divisor is 0. In a checked file each of these needs a reason it is fine, and the usual reason is a test you would write anyway.

t03_bounds.pychecked

def at_or(xs: list[int], i: Nat, default: int) -> int:
    if i < len(xs):
        return xs[i]
    return default


def average(xs: list[int]) -> int:
    if xs:
        return sum(xs) // len(xs)
    return 0


def find(xs: list[int], target: int) -> Nat:
    i = 0
    while i < len(xs) and xs[i] != target:
        i += 1
    return i


print(at_or([1, 2, 3], 1, 0), at_or([1, 2, 3], 9, 0), average([4, 8]), average([]), find([5, 6, 7], 7))

$ pagda t03_bounds.py

2 0 6 0 2

The checker reads the tests. Inside if i < len(xs): it knows the index is good. Inside if xs: it knows the list is not empty, so its length is not 0. In the while loop, the second part of the and relies on the first, as it does in Python.

Take the test away and the file is refused:

t03_bounds_bad.pyrefused

def average(xs: list[int]) -> int:
    return sum(xs) // len(xs)

$ pagda t03_bounds_bad.py

  File "t03_bounds_bad.py", line 6
    return sum(xs) // len(xs)
TypeCheckError: (len xs == 0) != false of type Bool
when checking that the expression refl has type
(pos (len xs) == pos 0) ≡ false
The checker cannot see that a condition this line relies on holds. xs[i] needs i < len(xs), d[k] needs k in d, // and % need a divisor that is not 0, a - b on Nats needs b <= a, and an assert inside a function needs its condition. known(c) gives the proof inside 'if c:' or 'while c:', with c written the same way. Put the code under an 'if' that tests it.

None

Optional[T] is a value that is a T or None. To use it as a T, test it first. After if found is None: return ..., the name holds a plain value.

t04_none.pychecked

def price(prices: dict[str, int], name: str) -> int:
    found = prices.get(name)          # an int, or None
    if found is None:
        return 0
    return found * 2                  # here it is an int


def longest(words: list[str]) -> Optional[str]:
    best = None
    for w in words:
        if best is None or len(w) > len(best):
            best = w
    return best


print(price({"pen": 3}, "pen"), price({"pen": 3}, "ink"), longest(["a", "ccc", "bb"]), longest([]))

$ pagda t04_none.py

6 0 ccc None

The second def never writes Optional for best. A local that is None in one place and a value in another is an Optional.

Changing a list

append, xs[i] = v and the other in-place changes work on a list the function made itself.

t05_change.pychecked

def squares(n: Nat) -> list[Nat]:
    out: list[Nat] = []
    for i in range(n):
        out.append(i * i)
    return out


def bumped(xs: list[int]) -> list[int]:
    ys = list(xs)                     # a copy that this function owns
    for i in range(len(ys)):
        ys[i] += 1
    return ys


print(squares(5), bumped([1, 2, 3]))

$ pagda t05_change.py

[0, 1, 4, 9, 16] [2, 3, 4]

A list that came in as a parameter belongs to the caller too. Changing it in place would change what the caller sees, so it is refused. Copy it first with list(xs).

t05_change_bad.pyrefused

def add_one(xs: list[int]) -> list[int]:
    xs.append(1)
    return xs

$ pagda t05_change_bad.py

  File "t05_change_bad.py", line 6
    xs.append(1)
TypeCheckError: 'xs' may be shared here: it is a parameter, or it came from a call, or it was given another name, passed on or put inside another value. A shared list or dict cannot be changed in place, because the other holder would see the change. Make a copy first: xs = list(xs)

Loops

A for loop needs nothing extra. A while loop has to end, and the checker sees that by itself for the two commonest shapes: a count going up to a limit, and a count going down to 0.

t06_loops.pychecked

def triangle(n: Nat) -> Nat:
    i = 0
    total = 0
    while i < n:
        total += i
        i += 1
    return total


def countdown(k: int) -> list[int]:
    out: list[int] = []
    while k > 0:
        out.append(k)
        k -= 1
    return out


print(triangle(5), countdown(3))

$ pagda t06_loops.py

10 [3, 2, 1]

Any other while loop ends with decreases(measure, proof), which names a number that gets smaller on every pass. Proofs shows one.

Values in types

This is where Pagda goes past ordinary type checkers. A type can mention a value. Vec[A, n] is a list of exactly n items, and dot takes two vectors of the same length.

t07_vec.pychecked

class Vec[A, n: Nat](Data): ...


@constructor
def Nil[A]() -> Vec[A, 0]: ...


@constructor
def Cons[A, n: Nat](head: A, tail: Vec[A, n]) -> Vec[A, n + 1]: ...


def dot[n: Nat](a: Vec[int, n], b: Vec[int, n]) -> int:
    match a:
        case Nil():
            return 0
        case Cons(x, xs):
            match b:
                case Cons(y, ys):
                    return x * y + dot(xs, ys)


v: Vec[int, 2] = Cons(1, Cons(2, Nil()))
w: Vec[int, 2] = Cons(3, Cons(4, Nil()))
print(dot(v, w))

$ pagda t07_vec.py

The second match has only one case. The checker knows b has the same length as a, so when a is a Cons, b is one too. Give dot vectors of different lengths and the file is refused:

t07_vec_bad.pyrefused

class Vec[A, n: Nat](Data): ...


@constructor
def Nil[A]() -> Vec[A, 0]: ...


@constructor
def Cons[A, n: Nat](head: A, tail: Vec[A, n]) -> Vec[A, n + 1]: ...


def dot[n: Nat](a: Vec[int, n], b: Vec[int, n]) -> int:
    match a:
        case Nil():
            return 0
        case Cons(x, xs):
            match b:
                case Cons(y, ys):
                    return x * y + dot(xs, ys)


v: Vec[int, 2] = Cons(1, Cons(2, Nil()))
w: Vec[int, 3] = Cons(3, Cons(4, Cons(5, Nil())))
print(dot(v, w))

$ pagda t07_vec_bad.py

  File "t07_vec_bad.py", line 28
    print(dot(v, w))
TypeCheckError: 3 != 2 of type Nat
when checking that the expression w has type Vec Int 2

Proofs

A return type can be a statement. add(n, 0) == n as a type means "a proof that add(n, 0) equals n". The body builds that proof, and a recursive call plays the part of the induction step.

t08_proof.pychecked

def add(a: Nat, b: Nat) -> Nat:
    if a == 0:
        return b
    return add(a - 1, b) + 1


# a fact about add, for every n. The return type is the fact.
def add_zero(n: Nat) -> add(n, 0) == n:
    if n == 0:
        return refl()                      # add(0, 0) is 0 by working it out
    return cong(suc, add_zero(n - 1))      # the fact for n - 1 gives the fact for n


assert add(20, 22) == 42                   # worked out by the checker
print(add(20, 22), add_zero(7))

$ pagda t08_proof.py

42 Refl()

An assert at the top level is worked out by the checker before the program runs. A false one is a type error.

Asking the caller for a reason

A def can take a proof as a parameter. at reads xs[i] with no test of its own, because its third parameter is a proof that i is in range. The caller gets that proof from its own test with known(...).

t09_param.pychecked

def at(xs: list[int], i: Nat, ok: (i < len(xs)) == True) -> int:
    return xs[i]                      # no test needed: the caller proved it


def third_or_zero(xs: list[int]) -> int:
    if 2 < len(xs):
        return at(xs, 2, known(2 < len(xs)))
    return 0


print(third_or_zero([7, 8, 9]), third_or_zero([7]))

$ pagda t09_param.py

9 0

A caller with no reason is refused:

t09_param_bad.pyrefused

def at(xs: list[int], i: Nat, ok: (i < len(xs)) == True) -> int:
    return xs[i]


def third(xs: list[int]) -> int:
    return at(xs, 2, refl())

$ pagda t09_param_bad.py

  File "t09_param_bad.py", line 10
    return at(xs, 2, refl())
TypeCheckError: (2 < len xs) != true of type Bool
when checking that the expression refl has type (2 < len xs) ≡ true

Holes

Write hole() for a part you have not worked out. The checker checks everything else, then says what the hole needs and what is in scope there.

t10_hole.pyrefused

def plus_zero(n: Nat) -> n + 0 == n:
    if n == 0:
        return refl()
    return cong(suc, hole())

$ pagda t10_hole.py

  File "t10_hole.py", line 8
    return cong(suc, hole())
TypeCheckError: this file has 1 hole, so it was not run.
line 8: hole() needs a value of type
  n₁ + 0 ≡ n₁
with these names to build it from:
  n₁ : Nat

Exceptions

raise and try work as in Python. The checker follows every exception to the clause that catches it, so a top-level assert about code that raises is still worked out before the program runs.

t12_exceptions.pychecked

class ParseError(Exception): ...


def digit(ch: str) -> int:
    table = {"0": 0, "1": 1, "2": 2, "3": 3, "4": 4, "5": 5, "6": 6, "7": 7, "8": 8, "9": 9}
    if ch in table:
        return table[ch]
    raise ParseError(f"not a digit: {ch}")


def parse(text: str) -> int:
    value = 0
    for ch in text:
        d = digit(ch)                 # can raise: the call stands on its own line
        value = value * 10 + d
    return value


def parse_or(text: str, default: int) -> int:
    try:
        n = parse(text)
    except ParseError as e:
        print("bad input:", e)
        return default
    except Exception:
        return default
    return n


assert parse_or("120", 0) == 120      # worked out by the checker, exceptions and all
print(parse_or("120", 0), parse_or("12x", -1))

$ pagda t12_exceptions.py

bad input: not a digit: x
120 -1

Two rules are new. A call to a def that can raise stands on its own line, as d = digit(ch) does. And a def that calls one is itself taken to raise unless a clause such as except Exception: catches everything.

The outside world

A checked file cannot open files or call libraries the checker has not read. A def marked @trusted is the door. The checker reads its annotations and believes them.

t11_trusted.pychecked

@trusted
def file_size(path: str) -> Nat:
    import os
    return os.path.getsize(path)


def is_big(path: str) -> bool:
    return 1000000 < file_size(path)

$ pagda --check t11_trusted.py

t11_trusted.py: no type errors

Checked files can also import each other: from shapes import Point, width.

Where next

Proofs goes further into types that state facts.
Examples has longer programs.
The reference lists everything a checked file can hold.